diff options
| -rw-r--r-- | generic/proof-config.el | 14 | ||||
| -rw-r--r-- | isa/isa.el | 11 |
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) @@ -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." |