diff options
author | 2002-01-16 16:05:22 +0000 | |
---|---|---|
committer | 2002-01-16 16:05:22 +0000 | |
commit | 31e269e30031321c4ee9e9ac03f33207df236044 (patch) | |
tree | 529fd867c75f1ed0a3953580f7d8525466e02cb4 /isa | |
parent | 71ae23d37a289dc9732576bc0ac4daef96be71df (diff) |
Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp
Diffstat (limited to 'isa')
-rw-r--r-- | isa/isa.el | 11 |
1 files changed, 3 insertions, 8 deletions
@@ -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." |