diff options
author | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-03 10:08:30 +0000 |
---|---|---|
committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-03 10:08:30 +0000 |
commit | 6549a40f3ab0eefdcd827ed4449884239c0bf2b2 (patch) | |
tree | de6794cce42463104edca51b1cca1f2c8c2ab51e /generic/proof-shell.el | |
parent | 19f16ac8eb742ff6337626b9d46c308ffa3e63a8 (diff) |
A* Fix display handling problems (tms, all week)
Done. :-)
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r-- | generic/proof-shell.el | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b2e6dd30..da88bf30 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -363,6 +363,9 @@ This is a list of tuples of the form (type . string). type is either (incf ip)) (set-buffer proof-pbp-buffer) (erase-buffer) + ;; Perhaps we ought to erase the proof-response-buffer at this + ;; point as well. It may contain an error message referring to + ;; an *earlier* state in the proof. (insert (substring out 0 op)) (proof-display-and-keep-buffer proof-pbp-buffer) @@ -491,6 +494,8 @@ we call `proof-shell-handle-error-hook'. " (cdr proof-shell-delayed-output))) (proof-display-and-keep-buffer proof-pbp-buffer))) + ;; Perhaps we should erase the buffer in proof-response-buffer, too? + ;; We extract all text between text matching ;; `proof-shell-error-regexp' and the following prompt. ;; Alternatively one could higlight all output between the |