diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 14:44:43 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 14:44:43 +0000 |
| commit | ce8067bac33f7d7f343b481e1d6e44216a1993c7 (patch) | |
| tree | 0dd74607d8965ff51b7196bf7b5e4476018c8d56 /generic/proof-shell.el | |
| parent | e621111d078b17a0fa689d01a71074e386a1f150 (diff) | |
Begin support for thms buffer
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index d15315be..ecaa1817 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -260,20 +260,21 @@ Does nothing if proof assistant is already running." (setq proof-shell-buffer nil) (error "Starting process: %s..failed" proof-prog-name)) + ;; FIXME: patch to go in here to clean this up ;; Create the associated buffers and set buffer variables (let ((goals (concat "*" proc "-goals*")) (resp (concat "*" proc "-response*")) - (trace (concat "*" proc "-trace*"))) - + (trace (concat "*" proc "-trace*")) + (thms (concat "*" proc "-thms*"))) (setq proof-goals-buffer (get-buffer-create goals)) (setq proof-response-buffer (get-buffer-create resp)) - ;; Only make a trace buffer if the prover may use it. (if proof-shell-trace-output-regexp (setq proof-trace-buffer (get-buffer-create trace))) - + (if proof-shell-thms-output-regexp + (setq proof-thms-buffer (get-buffer-create thms))) ;; Set the special-display-regexps now we have the buffer names (setq proof-shell-special-display-regexp - (proof-regexp-alt goals resp trace)) + (proof-regexp-alt goals resp trace thms)) (proof-multiple-frames-enable)) (save-excursion |