ignore 3-pane mode if frame is too small

Fixes ProofGeneral#760.

ci/simple-tests/coq-test-three-window.el

@@ -16,14 +16,17 @@
 ;; three times `window-min-height' (which defaults to 4). The problem
 ;; was relevant for Emacs 26.3, 27.1, and 27.2 running in batch mode
 ;; in docker containers, because they set their frame height to 9 (and
-;; their width to 10). For this reason most Proof General CI tests
-;; disable three pane mode in one or the other way.
+;; their width to 10) in such environments. For this reason most Proof
+;; General CI tests disable three pane mode in one or the other way.
 ;;
-;; This file tests the internal function `proof-select-three-b' that
-;; contains the bug and one user command affected by the bug
-;; (`proof-toggle-active-scripting') with three different frame sizes:
-;; too small for 3 windows, just big enough for 3 windows, and the
-;; default frame size. 
+;; This file tests that the internal function `proof-select-three-b'
+;; creates 3 windows if the frame height is big enough. Additionally,
+;; it is tested that one user command
+;; (`proof-toggle-active-scripting') that used to be affected by the
+;; bug does not signal an error, regardless of the frame size. Both
+;; functions are tested with three different frame sizes: too small
+;; for 3 windows, just big enough for 3 windows, and the default frame
+;; size.
 
 (require 'pg-response)
 
@@ -39,51 +42,64 @@ source file."
     (message "Coq and Proof General reseted")))
 
 
-(defun test-proof-select-three-b-for-height (height)
+(defun test-proof-select-three-b-for-height (height expect-error)
   "Test `proof-select-three-b' in 3-pane mode for HEIGHT.
-The function should not signal an error and set up 3 windows."
-  (let ((b1 (get-buffer-create "test-b1"))
-        (b2 (get-buffer-create "test-b2"))
-        (b3 (get-buffer-create "test-b3"))
-        ;; the following is set to its default value
-        (proof-three-window-enable t))
-    (reset-coq)
-    (message "Check test-proof-select-three-b for height %d" height)
-    (set-frame-height (selected-frame) height)
-    (proof-select-three-b b1 b2 b3 'smart)
-    (message "Apparently no error signaled in proof-select-three-b")
-    (message "Check that there are 3 windows")
-    (should (eq (length (window-list)) 3))))
+EXPECT-ERROR must be non-nil precisely if the frame height is
+expected to be too small for 3 windows. In this case nothing is
+done here, because `proof-select-three-b' must not be called in
+such situations. Otherwise the function should not signal an
+error and set up 3 windows."
+  (if expect-error
+      (message "Skip test-proof-select-three-b for height %d" height)
+    (let ((b1 (get-buffer-create "test-b1"))
+          (b2 (get-buffer-create "test-b2"))
+          (b3 (get-buffer-create "test-b3"))
+          ;; the following is set to its default value
+          (proof-three-window-enable t))
+      (reset-coq)
+      (message "Check test-proof-select-three-b for height %d" height)
+      (set-frame-height (selected-frame) height)
+      (proof-select-three-b b1 b2 b3 'smart)
+      (message "Apparently no error signaled in proof-select-three-b")
+      (message "Check that there are 3 windows")
+      (should (eq (length (window-list)) 3))
+
+      ;; clean up
+      (kill-buffer b1)
+      (kill-buffer b2)
+      (kill-buffer b3))))
+
 
 (ert-deftest test-proof-select-three-b-too-small ()
   "Test `proof-select-three-b' for a frame height too small for 3 windows."
-  :expected-result :failed
-  (test-proof-select-three-b-for-height (- (* 3 window-min-height) 1)))
+  (test-proof-select-three-b-for-height (- (* 3 window-min-height) 1) t))
 
 (ert-deftest test-proof-select-three-b-just-big-enough ()
   "Test `proof-select-three-b' for a frame height just big enough for 3 windows."
-  (test-proof-select-three-b-for-height (* 3 window-min-height)))
+  (test-proof-select-three-b-for-height (* 3 window-min-height) nil))
 
 (ert-deftest test-proof-select-three-b-default-height ()
   "Test `proof-select-three-b' for the default frame height.
 Note that for Emacs 26.3, 27.1, and 27.2, the default frame
 height is 9 when running in a docker container."
-  :expected-result (if (and
-                        ;; >= 26.3
-                        (or (> emacs-major-version 26)
-                            (and (eq emacs-major-version 26)
-                                 (>= emacs-minor-version 3)))
-                        ;; < 28
-                        (< emacs-major-version 28))
-                       :failed
-                     :passed)
-  (test-proof-select-three-b-for-height (frame-height)))
+  (test-proof-select-three-b-for-height
+   (frame-height)
+   (if (and
+        ;; >= 26.3
+        (or (> emacs-major-version 26)
+            (and (eq emacs-major-version 26) (>= emacs-minor-version 3)))
+        ;; < 28
+        (< emacs-major-version 28))
+       t
+     nil)))
 
 
-(defun test-activate-scripting-for-height (height)
+(defun test-activate-scripting-for-height (height num-win)
   "Test `proof-toggle-active-scripting' in 3-pane mode for HEIGHT.
-The function should not signal an error and there should be 3
-windows afterwards."
+The function should never signal an error and afterwards there
+should be 3 windows if the frame has enough space and 2
+otherwise. Argument NUM-WIN specifies the expected number of
+windows for HEIGHT."
   (let ((proof-three-window-enable t)
         (proof-three-window-mode-policy 'smart))
     (reset-coq)
@@ -92,30 +108,29 @@ windows afterwards."
     (find-file "some_file.v")
     (proof-toggle-active-scripting)
     (message "Apparently no error signaled in proof-toggle-active-scripting")
-    (message "Check that there are 3 windows")
-    (should (eq (length (window-list)) 3))))
+    (message "Check that there are %d windows" num-win)
+    (should (eq (length (window-list)) num-win))))
 
 
 (ert-deftest test-proof-toggle-active-scripting-too-small ()
   "Test `proof-toggle-active-scripting' in a frame too small for 3 windows."
-  :expected-result :failed
-  (test-activate-scripting-for-height (- (* 3 window-min-height) 1)))
+  (test-activate-scripting-for-height (* 4 window-min-height) 2))
 
 (ert-deftest test-proof-toggle-active-scripting-just-big-enough ()
   "Test `proof-toggle-active-scripting' in a frame just enough for 3 windows."
-    (test-activate-scripting-for-height (* 3 window-min-height)))
+    (test-activate-scripting-for-height (+ (* 4 window-min-height) 1) 3))
 
 (ert-deftest test-proof-toggle-active-scripting-default-height ()
   "Test `proof-toggle-active-scripting' with the default frame size.
 Note that for Emacs 26.3, 27.1, and 27.2, the default frame
 height is 9 when running in a docker container."
-  :expected-result (if (and
-                        ;; >= 26.3
-                        (or (> emacs-major-version 26)
-                            (and (eq emacs-major-version 26)
-                                 (>= emacs-minor-version 3)))
-                        ;; < 28
-                        (< emacs-major-version 28))
-                       :failed
-                     :passed)
-  (test-activate-scripting-for-height (frame-height)))
+  (test-activate-scripting-for-height
+   (frame-height)
+   (if (and
+        ;; >= 26.3
+        (or (> emacs-major-version 26)
+            (and (eq emacs-major-version 26) (>= emacs-minor-version 3)))
+        ;; < 28
+        (< emacs-major-version 28))
+       2
+     3)))

doc/ProofGeneral.texi

@@ -3463,6 +3463,10 @@ If you use several frames (the same Emacs in several windows on the
 screen), you can force a frame to stick to showing the goals or
 response buffer.
 
+This option only takes effect if the frame height is bigger than
+4 times @samp{@code{window-min-height}} (i.e., bigger than 16 with default
+values) because there must be enough space to create 3 windows.
+
 The default value is @code{t}.
 @end defopt
 

generic/pg-response.el

@@ -146,7 +146,10 @@ See ‘proof-layout-windows’ for more details about POLICY."
   "Put the three buffers B1, B2, and B3 into three windows.
 Following POLICY, which can be 'smart, 'horizontal, 'vertical, or 'hybrid.
 
-See ‘proof-layout-windows’ for more details about POLICY."
+See ‘proof-layout-windows’ for more details about POLICY.
+
+This function must not be called if the frame has not enough
+space for 3 windows (see `window-min-height')."
   (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
   (delete-other-windows)
   (switch-to-buffer b1)
@@ -187,7 +190,10 @@ See ‘proof-layout-windows’ for more details about POLICY."
 
 (defun proof-display-three-b (&optional policy)
   "Layout three buffers in a single frame.  Only do this if buffers exist.
-In this case, call ‘proof-select-three-b’ with argument POLICY."
+In this case, call ‘proof-select-three-b’ with argument POLICY.
+
+This function must not be called if the frame has not enough
+space for 3 windows (see `window-min-height')."
   (interactive)
   (when (and (buffer-live-p proof-goals-buffer)
 	     (buffer-live-p proof-response-buffer))
@@ -272,7 +278,11 @@ dragging the separating bars.
     ;; Restore an existing frame configuration (seems buggy, typical)
     (if pg-frame-configuration
 	(set-frame-configuration pg-frame-configuration 'nodelete)))
-   (proof-three-window-enable ; single frame
+   ((and proof-three-window-enable ; single frame
+         ;; The minimal frame size for setting up 3 windows is 3 *
+         ;; window-min-height, obviously. Use a slightly bigger margin
+         ;; here.
+         (> (frame-height) (* 4 window-min-height)))
     ;; If we are coming from multiple frame mode, delete associated
     ;; frames (and only them).
     (proof-delete-all-associated-windows)

generic/proof-useropts.el

@@ -176,7 +176,11 @@ Emacs automatically resizing windows between proof steps.
 
 If you use several frames (the same Emacs in several windows on the
 screen), you can force a frame to stick to showing the goals or
-response buffer."
+response buffer.
+
+This option only takes effect if the frame height is bigger than
+4 times `window-min-height' (i.e., bigger than 16 with default
+values) because there must be enough space to create 3 windows."
   :type 'boolean
   :set 'proof-set-value
   :group 'proof-user-options)