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 ac1978740..339605ea4 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)