diff options
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | isa/isa.el | 5 | ||||
| -rw-r--r-- | isar/isar.el | 5 |
3 files changed, 11 insertions, 6 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 0028022b..ce9d99de 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1882,8 +1882,8 @@ This is an experimental feature, currently work-in-progress." :type '(choice nil regexp) :group 'proof-shell) -(defcustom proof-shell-spill-output-regexp nil - "Regexp matching tracing output which is ``spilled'' into trace buffer. +(defcustom proof-shell-trace-output-regexp nil + "Regexp matching tracing output which should be displayed in trace buffer. Each line which matches this regexp but would otherwise be treated as an ordinary response, is sent to the trace buffer instead of the response buffer. @@ -1892,6 +1892,8 @@ This is intended for unusual debugging output from the prover, rather than ordinary output from final proofs. Set to nil to disable. + +Suggestion: this can be set a function called by `proof-pre-shell-start-hook'." :type '(choice nil regexp) :group 'proof-shell) @@ -1992,6 +1994,7 @@ shell variables: proof-mode-for-shell proof-mode-for-response proof-mode-for-goals + proof-shell-trace-output-regexp This is the bare minimum needed to get a shell buffer and its friends configured in the function proof-shell-start." @@ -202,7 +202,7 @@ and script mode." proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-start-length 1 proof-shell-eager-annotation-end "\361\\|\363" - proof-shell-trace-output-regexp "\375" + ;; see isa-pre-shell-start for proof-shell-trace-output-regexp ;; Some messages delimited by eager annotations proof-shell-clear-response-regexp "Proof General, please clear the response buffer." @@ -548,7 +548,8 @@ you will be asked to retract the file or process the remainder of it." (setq proof-prog-name (isabelle-command-line)) (setq proof-mode-for-shell 'isa-shell-mode) (setq proof-mode-for-goals 'isa-goals-mode) - (setq proof-mode-for-response 'isa-response-mode)) + (setq proof-mode-for-response 'isa-response-mode) + (setq proof-shell-trace-output-regexp "\375")) (defun isa-mode-config () (isa-mode-config-set-variables) diff --git a/isar/isar.el b/isar/isar.el index 7a290ebf..af7ba7c1 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -205,7 +205,7 @@ proof-shell-eager-annotation-start-length 1 proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-end "\361\\|\363" - proof-shell-trace-output-regexp "\375" + ;; see isar-pre-shell-start for proof-shell-trace-output-regexp ;; Some messages delimited by eager annotations proof-shell-clear-response-regexp "Proof General, please clear the response buffer." @@ -479,7 +479,8 @@ proof-shell-retract-files-regexp." (setq proof-prog-name (isabelle-command-line)) (setq proof-mode-for-shell 'isar-shell-mode) (setq proof-mode-for-goals 'isar-goals-mode) - (setq proof-mode-for-response 'isar-response-mode)) + (setq proof-mode-for-response 'isar-response-mode) + (setq proof-shell-trace-output-regexp "\375")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |