Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer.

1 files changed, 15 insertions, 3 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 8989b695..39f139f6 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -425,17 +425,29 @@ Ensure that point is visible in window."
     (save-excursion
       (set-buffer buffer)
       ;; Here's a hack: if we're asking to display BUFFER from a
-      ;; secondary window, and the (next) other one is displaying the
+      ;; secondary window and the (next) other one is displaying the
       ;; script buffer, then we do switch-buffer instead.  This means
       ;; that goals and response buffer are swapped as expected in
       ;; two-pane mode even if either one is used to "drive" the
       ;; scripting.
+      ;; FIXME: would be better to deduce here which buffer
+      ;; we're displaying, and use windows-of-buffer to do
+      ;; something sensible.
       (if (and 
 	   (not proof-dont-switch-windows)
 	   (not (eq (next-window) (selected-window)))
-	   (eq (window-buffer (next-window))
+	   (eq (window-buffer (next-window nil 'ignoreminibuf))
 	       proof-script-buffer))
-	  (set-window-buffer (selected-window) buffer)
+	  (if (eq (selected-window) (minibuffer-window))
+	      ;; 17.8.01: avoid switching the minibuffer's contents 
+	      ;; -- terrrible confusion -- use next-window after
+	      ;; script buffer instead.
+	      ;; (another hack which is mostly right)
+	      (set-window-buffer 
+	       (next-window 
+		(car-safe (windows-of-buffer proof-script-buffer))
+		'ignoreminibuf) buffer)
+	    (set-window-buffer (selected-window) buffer))
 	(display-buffer buffer))
       (setq window (get-buffer-window buffer 'visible))
       (set-window-dedicated-p window proof-dont-switch-windows)