Changed the behaviour of proof-layout-windows. Now it follows the

'horizontal 'vertical 'smart policy.

3 files changed, 50 insertions, 18 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3b27180b..aad46d45 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -80,7 +80,11 @@
 ;; Common part (scrit, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
-    ["Toggle 3 windows mode" proof-three-window-toggle t]
+    ["Toggle 3 windows mode" proof-three-window-toggle 
+     :style toggle
+     :selected proof-three-window-enable
+     :help "Toggles the use of separate windows or frames for Coq responses and goals."
+     ]
     ["Refresh windows layout" proof-layout-windows t]
     ["Toggle tooltips" proof-output-tooltips-toggle
      :style toggle
diff --git a/generic/pg-response.el b/generic/pg-response.el
index c95d8cce..d6bf8651 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -109,22 +109,32 @@ Internal variable, setting this will have no effect!")
 (defun proof-three-window-enable ()
   (proof-layout-windows))
 
-(defun proof-select-three-b (b1 b2 b3 &optional nohorizontalsplit)
-  "Put the given three buffers into three windows."
+(defun proof-select-three-b (b1 b2 b3 &optional policy)
+  "Put the given three buffers into three windows.
+Following POLICY, which can be one of 'smart, 'horizontal, 'vertical."
   (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
   (delete-other-windows)
-  (if nohorizontalsplit
-      (proof-safe-split-window-vertically)
-    (split-window-horizontally))
   (switch-to-buffer b1)
-  (other-window 1)
-  (proof-safe-split-window-vertically)
-  (switch-to-buffer b2)
-  (other-window 1)
-  (switch-to-buffer b3)
-  (other-window 1))
-
-(defun proof-display-three-b (&optional nohorizontalsplit)
+  (save-selected-window
+    (cond
+     ((eq policy 'horizontal)
+      (split-window-horizontally)
+      (other-window 1)
+      (switch-to-buffer b2))
+     ((eq policy 'vertically)
+      (split-window-vertically)
+      (other-window 1)
+      (switch-to-buffer b2))
+     ((or (null policy) (eq policy 'smart))
+      (display-buffer b2) ; horizontally if frame large enough
+      (other-window 1)))
+    (proof-safe-split-window-vertically) ; enlarge vertically if necessary
+    (other-window 1)
+    (switch-to-buffer b3)))
+
+
+
+(defun proof-display-three-b (&optional policy)
   "Layout three buffers in a single frame.  Only do this if buffers exist."
   (interactive)
   (when (and (buffer-live-p proof-goals-buffer)
@@ -132,7 +142,7 @@ Internal variable, setting this will have no effect!")
     (save-excursion
       (proof-select-three-b
        proof-script-buffer proof-goals-buffer proof-response-buffer
-       nohorizontalsplit))))
+       policy))))
 
 (defvar pg-frame-configuration nil
   "Variable storing last used frame configuration.")
@@ -142,7 +152,7 @@ Internal variable, setting this will have no effect!")
   "Cache the current frame configuration, between prover restarts."
   (setq pg-frame-configuration (current-frame-configuration)))
 
-(defun proof-layout-windows (&optional nohorizontalsplit)
+(defun proof-layout-windows ()
   "Refresh the display of windows according to current display mode.
 
 For single frame mode, this uses a canonical layout made by splitting
@@ -156,7 +166,7 @@ full width of the Emacs frame.
 
 For multiple frame mode, this function obeys the setting of
 `pg-response-eagerly-raise', which see."
-  (interactive "P")
+  (interactive)
   (cond
    (proof-multiple-frames-enable
     (delete-other-windows) ;; hope we're on the right frame/window
@@ -171,7 +181,7 @@ For multiple frame mode, this function obeys the setting of
    (proof-three-window-enable
     (proof-delete-other-frames)
     (set-window-dedicated-p (selected-window) nil)
-    (proof-display-three-b nohorizontalsplit))
+    (proof-display-three-b proof-three-window-mode-policy))
    ;; Two-of-three window mode.
    ;; Show the response buffer as first in preference order.
    (t
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 206ea9da..e6712ff6 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -177,6 +177,24 @@ and displayed lazily.  See `proof-layout-windows'."
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defcustom proof-three-window-mode-policy 'smart
+  "*Window splitting policy for three window mode.
+- If 'vertical then never split horizontally.
+- If 'horizontal then always have scripting buffer on the right
+  and goal and response buffers on the left (one above the
+  other).
+- If 'smart or anything else means: 'horizontal when the window
+  is wide enough and horizontally otherwise. The widht threshold
+  is given by `split-width-threshold'.
+
+  See `proof-layout-windows'."
+  :type '(choice
+	  (const :tag "Horizontally if frame wide enough" smart)
+	  (const :tag "Horizontally" horizontal)
+	  (const :tag "Vertically" vertical))
+  :group 'proof-user-options)
+
+
 (defcustom proof-delete-empty-windows nil
   "*If non-nil, automatically remove windows when they are cleaned.
 For example, at the end of a proof the goals buffer window will