Refresh response buffer when goals buffer is refreshed.

1 files changed, 6 insertions, 3 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 78e60a7c..0c3f7916 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -365,11 +365,14 @@ This is a list of tuples of the form (type . string). type is either
 	    (progn (aset out op c)
 		   (incf op)))
 	(incf ip))
+
+      ;; Response buffer may be out of date. It may contain (error)
+      ;; messages relating to earlier proof states
+      (set-buffer proof-response-buffer)
+      (erase-buffer)
+
       (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)