Fixing #121 + avoid hiding user windows too much.

2 files changed, 56 insertions, 34 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 484ee0d5..893d1f6f 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -158,23 +158,29 @@ Following POLICY, which can be one of 'smart, 'horizontal,
       (other-window 1)
       (switch-to-buffer b2)
       (proof-safe-split-window-vertically) ; enlarge vertically if necessary
+      (set-window-dedicated-p (selected-window) proof-three-window-enable)
       (other-window 1)
-      (switch-to-buffer b3))
+      (switch-to-buffer b3)
+      (set-window-dedicated-p (selected-window) proof-three-window-enable))
      ((eq pol 'vertical)
       (split-window-vertically)
       (other-window 1)
       (switch-to-buffer b2)
       (proof-safe-split-window-vertically) ; enlarge vertically if necessary
+      (set-window-dedicated-p (selected-window) proof-three-window-enable)
       (other-window 1)
-      (switch-to-buffer b3))
+      (switch-to-buffer b3)
+      (set-window-dedicated-p (selected-window) proof-three-window-enable))
      ((eq pol 'horizontal)
       (split-window-horizontally) ; horizontally again
       (other-window 1)
       (switch-to-buffer b2)
       (enlarge-window (/ (frame-width) 6) t) ; take 2/3 of width before splitting again
       (split-window-horizontally) ; horizontally again
+      (set-window-dedicated-p (selected-window) proof-three-window-enable)
       (other-window 1)
-      (switch-to-buffer b3))))))
+      (switch-to-buffer b3)
+      (set-window-dedicated-p (selected-window) proof-three-window-enable))))))
 
 
 
@@ -271,7 +277,7 @@ dragging the separating bars.
     (proof-delete-all-associated-windows)
     (set-window-dedicated-p (selected-window) nil)
     (proof-display-three-b proof-three-window-mode-policy))
-   ;; Two-of-three window mode.
+   ;; Two window mode.
    ;; Show the response buffer as first in preference order.
    (t
     ;; If we are coming from multiple frame mode, delete associated
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index be5fee6e..75ddbf69 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -220,43 +220,59 @@ Leave point at END."
   (unless (and (boundp sym) (symbol-value sym))
     (warn "Proof General %s: %s is unset."  tag (symbol-name sym))))
 
+(defvar proof-advertise-layout-freq 30
+  "Frequency for PG messages to be displayed from time to time.")
+(defvar proof-advertise-layout-count proof-advertise-layout-freq
+  "counter used to display PG messages from time to time.")
+
 (defun proof-get-window-for-buffer (buffer)
   "Find a window for BUFFER, display it there, return the window.
-NB: may change the selected window."
+NB: may change the selected window. This function is a wrapper on
+display-buffer. The idea is that if the user has opened and
+closed some windows we want to preserve the layout by only
+switching buffer in already pg-associate windows. So if the
+buffer is not already displayed, we try to reuse an existing
+associated window, even if in 3-win mode. If no such window
+exists, we fall back to display-buffer while protecting script
+buffer to be hidden or split.
+
+Experimentally we display a message from time to time advertising
+C-c C-l."
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
-    ;; THEN find somewhere nice to display it
-	  (if (and
-	     ;; If we're in two-window mode and already displaying a
-	     ;; script/response/goals, try to just switch the buffer
-	     ;; instead of calling display-buffer which alters sizes.
-	     ;; Gives user some stability on display.
-	     (not proof-three-window-enable)
-	     (> (count-windows) 1)
-	     ;; was: (not (eq (next-window) (selected-window)))
-	     (memq (window-buffer (next-window nil 'ignoreminibuf))
-		   ;; NB: 3.5: added rest of assoc'd buffers here
-		   (cons proof-script-buffer (proof-associated-buffers))))
-	    (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 (get-buffer-window-list proof-script-buffer))
-		  'ignoreminibuf) buffer)
-	      (if (eq (window-buffer (next-window nil 'ignoreminibuf))
-		      proof-script-buffer)
-		  ;; switch this window
-		  (set-window-buffer (selected-window) buffer)
-		;; switch other window
-		(set-window-buffer (next-window nil 'ignoreminibuf) buffer)))
-	    ;; o/w: call display buffer to configure windows nicely.
-	    (display-buffer buffer)))
+    (if proof-three-window-enable
+        (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count)
+          (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout"))
+          (setq proof-advertise-layout-count 0)))
+    ;; THEN either we are in 2 wins mode and we must switch the assoc
+    ;; window to buffer OR we deleted a window by mistake and we
+    ;; behave as if in 2 win mode instead of calling display-buffer
+    ;; (stability for the user). If no assoc win exists then we are in
+    ;; trouble: let display-buffer decide but avoid hiding the script buffer.
+    (if (= (count-windows) 1)
+        ;; only one window: fallback to display-buffer
+        (display-buffer buffer)
+      ;; There is at least 2 windows, let us find some assoc ones.
+      (let* ((assoc-wins (proof-associated-windows))
+             ;; may be nil if no assoc frame
+             (win-to-use (and assoc-wins (car assoc-wins))))
+        ;; let us switch the buffer in this window even if protected (3-win mode)
+        (if win-to-use
+            (let ((prot (window-dedicated-p win-to-use)))
+              (set-window-dedicated-p win-to-use nil)
+              (set-window-buffer win-to-use buffer)
+              (set-window-dedicated-p win-to-use prot))
+          ;; if no assoc win then let display-buffer decide but
+          ;; protect script buffer from disappearing.
+          (let ((win-proof-script (car-safe (get-buffer-window-list proof-script-buffer))))
+            (set-window-dedicated-p win-proof-script t) ; avoid to hide script buffer at all cost
+            (let ((res (display-buffer buffer))) ; return this but revert the dedicated flag first
+              (set-window-dedicated-p win-proof-script nil)
+              res))))))
   ;; Return the window, hopefully the one we first thought of.
   (get-buffer-window buffer 0))
 
+
 (defun proof-display-and-keep-buffer (buffer &optional pos force)
   "Display BUFFER and make window according to display mode.
 If optional POS is present, will set point to POS.