diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2001-12-05 15:36:23 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2001-12-05 15:36:23 +0000 |
| commit | 5721c119ad270b128f8770afbef8a691befd4ed0 (patch) | |
| tree | 73a069664af274cf5c8d91c3c142a0b9c57b116d /generic | |
| parent | 990f07fb23220c8294c1090e6d44bd0c5a7dda18 (diff) | |
proof-release-lock: do not touch proof-shell-spill-output-buffer;
proof-shell-spill-output-begin: reuse existing buffer;
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c9ea37f7..60bcd2d7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -136,8 +136,7 @@ If QUEUEMODE is supplied, set the lock to that value." Clear proof-shell-busy, and set proof-shell-error-or-interrupt-seen to err-or-int." (setq proof-shell-error-or-interrupt-seen err-or-int) - (setq proof-shell-busy nil) - (setq proof-shell-spill-output-buffer nil)) + (setq proof-shell-busy nil)) @@ -1554,9 +1553,9 @@ This is a subroutine of proof-shell-filter." (defun proof-shell-spill-output-begin (msg) "Begin spill output from prover into a fresh response-like buffer." (let* ((spill (concat "*" (downcase proof-assistant) "-trace*"))) - ;; FIXME: maybe this should always be the same buffer, proliferation - ;; is maybe confusing. - (setq proof-shell-spill-output-buffer (generate-new-buffer spill)) + (or (buffer-live-p proof-shell-spill-output-buffer) + (setq proof-shell-spill-output-buffer + (generate-new-buffer spill))) (save-excursion (set-buffer proof-shell-spill-output-buffer) (funcall proof-mode-for-response) |