A* Fix display handling problems (tms, all week)

Done. :-)

2 files changed, 25 insertions, 15 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
diff --git a/generic/proof.el b/generic/proof.el
index 440c2ab8..ef3e68a6 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -151,21 +151,26 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
 
 
 (defun proof-display-and-keep-buffer (buffer)
-  "Display BUFFER and mark window according to `proof-window-dedicated-p'."
-  (let ((window (get-buffer-window buffer 'visible)))
-    (save-selected-window
-      (save-excursion 
-	(display-buffer buffer)
-	(set-window-dedicated-p (get-buffer-window buffer)
-				proof-window-dedicated-p)
-	(and window
-	     (progn (select-window window)
-		    ;; tms: I don't understand why the point in
-		    ;; proof-response-buffer is not at the end anyway.
-		    ;; Is there a superfluous save-excursion somewhere?
-		    (set-buffer buffer)
-		    (goto-char (point-max))
-		    (or (pos-visible-in-window-p) (recenter -1))))))))
+  "Display BUFFER and mark window according to `proof-window-dedicated-p'.
+
+Also ensures that point is visible."
+  (let (window)
+    (save-excursion
+      (set-buffer buffer)
+      (display-buffer buffer)
+      (setq window (get-buffer-window buffer 'visible))
+      (set-window-dedicated-p window proof-window-dedicated-p)
+      (and window
+	   (save-selected-window
+	     (select-window window)
+	     
+	     ;; tms: I don't understand why the point in
+	     ;; proof-response-buffer is not at the end anyway.
+	     ;; Is there a superfluous save-excursion somewhere?
+	     (goto-char (point-max))
+
+	     (or (pos-visible-in-window-p (point) window)
+		 (recenter -1)))))))
 
 (defun proof-clean-buffer (buffer)
   "Erase buffer and hide from display."