Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp

2 files changed, 11 insertions, 14 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 85247eda..0028022b 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1883,13 +1883,15 @@ This is an experimental feature, currently work-in-progress."
   :group 'proof-shell)
 
 (defcustom proof-shell-spill-output-regexp nil
-  "Regexp matching output which is to be ``spilled'' into new buffer.
-This allows the prover to output tracing messages, and the like,
-into a new buffer.   The end of the spilled output is the next
-prompt.  This is intended for unusual debugging output from the
-prover, rather than ordinary output from final proofs.  
+  "Regexp matching tracing output which is ``spilled'' into 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.   
+
+This is intended for unusual debugging output from 
+the prover, rather than ordinary output from final proofs.  
+
 Set to nil to disable.
-This is an experimental feature, currently work-in-progress."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
diff --git a/isa/isa.el b/isa/isa.el
index 6f68ef76..f20590cd 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -197,17 +197,12 @@ and script mode."
    proof-shell-restart-cmd		"ProofGeneral.isa_restart();"
    proof-shell-quit-cmd			"quit();"
 
+   ;; NB: the settings below will only recognize tracing output in
+   ;; Isabelle 2001.
    proof-shell-eager-annotation-start   "\360\\|\362"
    proof-shell-eager-annotation-start-length 1
    proof-shell-eager-annotation-end     "\361\\|\363"
-   ;; ALTERNATIVE SETTINGS FOR TESTING TRACING MODE:
-   ;; FIXME: Isabelle should markup Applying message now as an
-   ;; eager annotation.
-   ;; proof-shell-eager-annotation-start   "\360\\|\362\\|Applying"
-   ;; proof-shell-spill-output-regexp      "Applying"
-   ;; proof-shell-eager-annotation-start-length 8 ;; was 1 (ideal)
-   ;; proof-shell-eager-annotation-end     "\361\\|\363\\|rule:"
-   ;; END TRACING TEST
+   proof-shell-spill-output-regexp      "\375"
 
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."