Set proof-shell-trace-output-regexp in proof-pre-shell-start-hook

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."
diff --git a/isa/isa.el b/isa/isa.el
index bd3cea9f..245c17d0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -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"))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;