From 6549a40f3ab0eefdcd827ed4449884239c0bf2b2 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 3 Nov 1998 10:08:30 +0000
Subject: A* Fix display handling problems  (tms, all week)

Done. :-)
---
 generic/proof-shell.el | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'generic/proof-shell.el')

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
-- 
cgit v1.2.3