From fc4416c76ffb50b29350c15c168939a33a1ec1eb Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Wed, 17 Apr 2024 09:22:44 +0200
Subject: [PATCH] ignore 3-pane mode if frame is too small
Fixes #760.
---
ci/simple-tests/coq-test-three-window.el | 119 +++++++++++++----------
doc/ProofGeneral.texi | 4 +
generic/pg-response.el | 16 ++-
generic/proof-useropts.el | 6 +-
4 files changed, 89 insertions(+), 56 deletions(-)
diff --git a/ci/simple-tests/coq-test-three-window.el b/ci/simple-tests/coq-test-three-window.el
index 972bb1f68..4b407e954 100644
--- a/ci/simple-tests/coq-test-three-window.el
+++ b/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)))
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index c0158d63c..3d1eac28d 100644
--- a/doc/ProofGeneral.texi
+++ b/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
diff --git a/generic/pg-response.el b/generic/pg-response.el
index cd611ad94..3381b4ea9 100644
--- a/generic/pg-response.el
+++ b/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)
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 7df22040e..0cc92637b 100644
--- a/generic/proof-useropts.el
+++ b/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)