diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 05:28:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 05:28:17 +0000 |
| commit | 2a23e37ad31880808de5881eedb3f9846265e1a1 (patch) | |
| tree | 89f2637b91070e939e22e7f3a2479beef947ab19 /generic | |
| parent | e5aba6d81e99a4e37026445cc63be52aeed1729a (diff) | |
Comment about proof-goals-display-qed-message mess.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 0a4f69ce..73d4b31a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -764,7 +764,7 @@ See the documentation for `proof-shell-delayed-output' for further details." ;; FIXME: this can be done away with, probably. (unless proof-shell-leave-annotations-in-output (setq str (proof-shell-strip-special-annotations str))) - + (proof-shell-maybe-erase-response t nil) (proof-response-buffer-display str) (proof-display-and-keep-buffer proof-response-buffer)) @@ -928,9 +928,12 @@ the proof assistant." (setq proof-shell-delayed-output (cons 'insert "\nAborted\n")) ()) - ;; FIXME: remove proof-goals-display-qed-message setting after 3.0, - ;; by matching on completed-regexp as an extra step, after - ;; errors/interrupt, but as well as ordinary output. + ;; FIXME: remove proof-goals-display-qed-message setting in version 3.2, + ;; by matching on completed-regexp as an extra step again when a goal + ;; is found, or alternatively in same part as errors/interrupt + ;; (but that risks displaying no subgoals message twice in Isabelle!). + ;; We can also remove the match-string 1 mess too, modify every + ;; instance accordingly. ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string) (proof-clean-buffer proof-goals-buffer) (setq proof-shell-proof-completed 0) ; counts commands since proof complete. |