From b984de69bb4fd5f10aa9a41a3da801bf5297d724 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 2 Mar 2024 18:07:00 +0100 Subject: [PATCH 1/5] coq: run silently and explicitly Show when necessary This is a step towards fixing #568. It fixes the cases after Proof, comments and auto, leaving now 3 instead of 6 failing tests in ci/simple-tests/test-goals-present.el. --- ci/simple-tests/coq-test-goals-present.el | 3 - coq/coq.el | 88 +++++++++++++++++------ generic/proof-shell.el | 6 +- 3 files changed, 72 insertions(+), 25 deletions(-) diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index e0784f1ba..520c5a3f9 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -151,17 +151,14 @@ goals buffer is not empty afterwards." (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." - :expected-result (if coq--post-v87 :failed :passed) (goals-after-test coq-src-proof "Proof")) (ert-deftest goals-after-comment () "Test goals are present after a comment." - :expected-result :failed (goals-after-test coq-src-comment "comment")) (ert-deftest goals-after-auto () "Test goals are present after ``auto''." - :expected-result (if coq--post-v87 :failed :passed) (goals-after-test coq-src-auto "auto")) (ert-deftest goals-after-simpl () diff --git a/coq/coq.el b/coq/coq.el index a036acde3..e21ccad27 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -122,8 +122,21 @@ Namely, goals that do not fit in the goals window." ;; should re-intialize to coq-search-blacklist-string instead of ;; keeping the current value (that may come from another file). ,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string)) - '("Set Suggest Proof Using. ") coq-user-init-cmd) - "Command to initialize the Coq Proof Assistant.") + '("Set Suggest Proof Using. " + "Set Silent. ") + coq-user-init-cmd) + "Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'. +List of commands sent to the Coq background process just after it +has been started. This happens inside `proof-shell-config-done', +when the major mode `coq-shell-mode' is configured in the `*coq*' +buffer. + +Sets silent mode. + +In normal interaction, the Coq is started because the user assert +some commands. Therefore the commands here are followed by those +inserted inside `proof-assert-command-hook', respectively, +`coq-adapt-printing-width'.") ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for ;; coq-script-parse-cmdend-forward/backward and coq-find-real-start. @@ -1207,12 +1220,18 @@ Printing All set." ;; command and *not* have the goal redisplayed, the command must be tagged with ;; 'empty-action-list. (defun coq-empty-action-list-command (cmd) - "Return the list of commands to send to Coq after CMD -if it is the last command of the action list. -If CMD is tagged with 'empty-action-list then this function won't -be called and no command will be sent to Coq. + "Return the list of commands to send to Coq if CMD is last in the action list. +Return the list of commands to be sent to Coq when +`proof-action-list' is empty, CMD was the last command just sent +to Coq and CMD was not tagged with `'empty-action-list'. Note: the last command added if `coq-show-proof-stepwise' is set -should match the `coq-show-proof-diffs-regexp'." +should match the `coq-show-proof-diffs-regexp'. + +When Coq runs silent, this function must return the necessary +Show commands to fill the `*goals*' buffer inside a proof. + +This function is called from `proof-shell-exec-loop' via +`proof-shell-empty-action-list-command'." (cond ((or ;; If closing a nested proof, Show the enclosing goal. @@ -1221,32 +1240,39 @@ should match the `coq-show-proof-diffs-regexp'." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) + ;; (message "coq-empty-action-list case 1") `("Show." . ,(coq--show-proof-stepwise-cmds))) ((or - ;; If we go back in the buffer and the number of abort is less than - ;; the number of nested goals, then Unset Silent and Show the goal + ;; If we go back in the buffer and the number of abort is less than the + ;; number of nested goals, that is, if we are inside a proof, then Show + ;; the goal. (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) - `("Unset Silent." - ,(if (coq--post-v810) (coq-diffs) "Show.") - . ,(coq--show-proof-stepwise-cmds))) + ;; (message "coq-empty-action-list case 2") + (append + (if (coq--post-v810) (list (coq-diffs)) ()) + '("Show.") + (coq--show-proof-stepwise-cmds))) ((or - ;; If we go back in the buffer and not in the above case, then only Unset - ;; silent (there is no goal to show). Still, we need to "Set Diffs" again + ;; If we go back in the buffer and not in the above case, i.e., outside a + ;; proof, then only set the Diffs option. (string-match-p "BackTo\\s-" cmd)) - (if (coq--post-v810) - (list "Unset Silent." (coq-diffs) ) - (list "Unset Silent."))) + ;; (message "coq-empty-action-list case 3") + (if (coq--post-v810) (list (coq-diffs)) ())) + ((or ;; If starting a proof, Show Proof if need be (coq-goal-command-str-p cmd) ;; If doing (not closing) a proof, Show Proof if need be (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0))) - (coq--show-proof-stepwise-cmds)))) + ;; (message "coq-empty-action-list case 4") + (append + '("Show.") + (coq--show-proof-stepwise-cmds))))) ;; This does not Set Printing Width, it rather tells pg to do that before each ;; command (if necessary) @@ -1326,7 +1352,9 @@ redisplayed." (let ((wdth (or width (coq-guess-goal-buffer-at-next-command)))) ;; if no available width, or unchanged, do nothing (when (and wdth (not (equal wdth coq-shell-current-line-width))) - (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t) + (proof-shell-invisible-command + (format "Set Printing Width %S." (- wdth 1)) + t nil 'empty-action-list) (setq coq-shell-current-line-width wdth) ;; Show iff show non nil and some proof is under way (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe))))) @@ -1943,8 +1971,11 @@ at `proof-assistant-settings-cmds' evaluation time.") ;; span menu (setq proof-script-span-context-menu-extensions #'coq-create-span-menu) - (setq proof-shell-start-silent-cmd "Set Silent. " - proof-shell-stop-silent-cmd "Unset Silent. ") + ;; When proof-shell-start-silent-cmd and proof-shell-stop-silent-cmd stay at + ;; their default value nil, the generic code won't switch Coq to silent and + ;; noisy at, respectively, the beginning and end of longer asserted regions. + ;; (setq proof-shell-start-silent-cmd "Set Silent. " + ;; proof-shell-stop-silent-cmd "Unset Silent. ") ;; prooftree config (setq @@ -1969,6 +2000,21 @@ at `proof-assistant-settings-cmds' evaluation time.") ) (defun coq-shell-mode-config () + "Initialization of `coq-shell-mode' that runs in the `*coq*' buffer. +The interaction buffer with Coq, `*coq*', uses a major mode that +is derived via `proof-shell-mode' from `scomint-mode'. This +function runs as the body of `coq-shell-mode' when the `*coq*' +buffer is initialized, which happens when the Coq background +process is started. This function intitalizes the Coq +personalization of Proof General in the interaction buffer with +Coq. At the end, this function calls `proof-shell-config-done', +which initializes the Coq session, e.g., by sending +`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq. + +In normal interaction, the proof assistant is started because the +user assert some commands. Therefore this function runs only +shortly before `proof-assert-command-hook', respectively, +`coq-adapt-printing-width'." (setq proof-shell-cd-cmd coq-shell-cd proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 4de85ddf9..57d538734 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -115,6 +115,8 @@ bother the user. They may include 'no-goals-display do not goals in *goals* buffer 'proof-tree-show-subgoal item inserted by the proof-tree package 'priority-action item added via proof-add-to-priority-queue + 'empty-action-list proof-shell-empty-action-list-command should not be + called if this is the last item in the action list Note that 'invisible does not imply any of the others. If flags are non-empty, interactive cues will be surpressed. (E.g., @@ -1070,7 +1072,9 @@ being processed." (unless (eq proof-shell-busy queuemode) (proof-debug "proof-append-alist: wrong queuemode detected for busy shell") - (cl-assert (eq proof-shell-busy queuemode))))) + (cl-assert + (eq proof-shell-busy queuemode) nil + "wrong queuemode in proof-add-to-queue: %s instead expected %s")))) (let ((nothingthere (null proof-action-list))) From 2d307a63d6b83f89a8399847d33322ae38a9ed32 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 3 Mar 2024 21:34:16 +0100 Subject: [PATCH 2/5] fix tests for preceding commit - update manuals - expect test goals-reset-after-admitted to fail again - expect errors in tests 020_coq-test-definition, 090_coq-test-regression-Fail and 091_coq-test-regression-Fail --- ci/coq-tests.el | 13 +++++++++++++ ci/simple-tests/coq-test-goals-present.el | 1 + doc/PG-adapting.texi | 2 ++ 3 files changed, 16 insertions(+) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 7f4291b16..d911f6e21 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -196,6 +196,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 020_coq-test-definition () + ;; There are no infomsgr when running silent. + :expected-result :failed "Test *response* output after asserting a Definition." (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -317,6 +319,10 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 090_coq-test-regression-Fail() + ;; When running silent, the message about indeed failing is not + ;; shown. One might fix this test by checking that there is no + ;; error, which would be shown without Fail. + :expected-result :failed "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -338,6 +344,13 @@ Tactic failure: Cannot solve this goal." "*coq*"))))) ;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*") (ert-deftest 091_coq-test-regression-Fail() + ;; XXX What is the difference between this test and + ;; 090_coq-test-regression-Fail? + + ;; When running silent, the message about indeed failing is not + ;; shown. One might fix this test by checking that there is no + ;; error, which would be shown without Fail. + :expected-result :failed "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index 520c5a3f9..c5d295135 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -171,6 +171,7 @@ goals buffer is not empty afterwards." (goals-after-test coq-src-error "error")) (ert-deftest goals-reset-after-admitted () + :expected-result :failed "The goals buffer is reset after an Admitted." (message "goals-reset-after-admitted: Check that goals are reset after Admitted.") diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 3e5e72e39..37aaaa518 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3890,6 +3890,8 @@ bother the user. They may include @code{'no-goals-display} do not goals in @strong{goals} buffer @code{'proof-tree-show-subgoal} item inserted by the proof-tree package @code{'priority-action} item added via @code{proof-add-to-priority-queue} + @code{'empty-action-list} @code{proof-shell-empty-action-list-command} should not be + called if this is the last item in the action list @end lisp Note that @code{'invisible} does not imply any of the others. If flags are non-empty, interactive cues will be surpressed. (E.g., From 1414157d79b89695960e228a896d69a593f57bb9 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 8 Mar 2024 10:42:26 +0100 Subject: [PATCH 3/5] CI test-goals-present: two more tests for resetting the goals buffer - goals should be reset when there are no more goals (does work) - goals should be reset after Qed (does not work) --- ci/simple-tests/coq-test-goals-present.el | 121 ++++++++++++++++------ 1 file changed, 87 insertions(+), 34 deletions(-) diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index c5d295135..e036bd969 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -67,13 +67,33 @@ Proof using. "Coq source code for checking goals after an error.") (defconst coq-src-admitted - "Lemma a : forall(P27X : Prop), P27X. + "Lemma a : forall(P : Prop), P. Proof using. - intros P27X. + intros P. Admitted. " "Coq source for checking that the goals buffer is reset after Admitted.") +(defconst coq-src-no-more-goals + " +Lemma a : 1 + 1 = 2. +Proof using. + simpl. + auto. +" + "Coq source code for checking that the goals buffer is reset when +no goals are left.") + +(defconst coq-src-qed + " +Lemma a : 1 + 1 = 2. +Proof using. + simpl. + auto. +Qed. +" + "Coq source code for checking that the goals buffer is reset after Qed.") + (defconst coq-src-update-goal-after-error " (* code taken from pull request #429 *) @@ -149,6 +169,61 @@ goals buffer is not empty afterwards." (set-buffer-modified-p nil)) (kill-buffer buffer))))) +(defun goals-buffer-should-be-empty (pos msg) + "Check that `*goals*' is empty after asserting/retracting to POS. +MSG is only used in a message, it should tell after which action +the goals buffer is expected to be empty." + (message "Check that goals buffer is empty after %s" msg) + (goto-char pos) + (proof-goto-point) + (wait-for-coq) + ;; (record-buffer-content "*coq*") + ;; (record-buffer-content "*goals*") + + ;; check that the goals buffer is empty + (with-current-buffer "*goals*" + (should (equal (point-min) (point-max))))) + +(defun goals-buffer-should-get-reset (coq-src coq-stm msg) + "Check that the goals buffer is reset. +Put the string COQ-SRC into a buffer and assert until the first +occurrence of COQ-STM, which should be a regular expression. At +this point the goals buffer needs to contain something. Then +assert to the end of COQ-SRC and check that the goals buffer has +been reset. MSG is used in messages only. It shouls say after +which action the goals buffer should have been reset." + (message "Check that goals are reset after %s." msg) + (setq proof-three-window-enable nil) + (let (buffer) + (unwind-protect + (progn + (find-file "goals.v") + (setq buffer (current-buffer)) + (insert coq-src) + + ;; First fill the goals buffer by asserting until the line + ;; after the first occurrence of COQ-STM. + + (goto-char (point-min)) + (should (re-search-forward coq-stm nil t)) + (forward-line 1) + (message "*goals* should be non-empty after asserting until after %s" + coq-stm) + (proof-goto-point) + (wait-for-coq) + ;; there should be something in the goals buffer now + (with-current-buffer "*goals*" + (should (not (equal (point-min) (point-max))))) + + (goals-buffer-should-be-empty (point-max) msg)) + + ;; clean up + (when buffer + (with-current-buffer buffer + (set-buffer-modified-p nil)) + (kill-buffer buffer))))) + + (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." (goals-after-test coq-src-proof "Proof")) @@ -173,40 +248,18 @@ goals buffer is not empty afterwards." (ert-deftest goals-reset-after-admitted () :expected-result :failed "The goals buffer is reset after an Admitted." - (message - "goals-reset-after-admitted: Check that goals are reset after Admitted.") - (setq proof-three-window-enable nil) - (let (buffer) - (unwind-protect - (progn - (find-file "goals.v") - (setq buffer (current-buffer)) - (insert coq-src-admitted) - - ;; Need to assert the Admitted alone, therefore first assert - ;; until before the Admitted. - (goto-char (point-min)) - (should (re-search-forward "intros P27X" nil t)) - (forward-line 1) - (proof-goto-point) - (wait-for-coq) + (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted")) - (forward-line 1) - (proof-goto-point) - (wait-for-coq) - ;; (record-buffer-content "*coq*") - ;; (record-buffer-content "*goals*") +(ert-deftest goals-reset-no-more-goals () + "The goals buffer is reset when there are no more goals." + (goals-buffer-should-get-reset coq-src-no-more-goals + "Proof using" "no more goals")) - ;; check that the old goal is not present in the goals buffer - (with-current-buffer "*goals*" - (goto-char (point-min)) - (should (not (re-search-forward "P27X" nil t))))) - - ;; clean up - (when buffer - (with-current-buffer buffer - (set-buffer-modified-p nil)) - (kill-buffer buffer))))) +(ert-deftest goals-reset-qed () + :expected-result :failed + "The goals buffer is reset after Qed." + (goals-buffer-should-get-reset coq-src-qed + "Proof using" "Qed")) (ert-deftest update-goals-after-error () "Test goals are updated after an error." From fb442fd31a36385503c92b735c6bc2c61aa3f697 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 7 Apr 2024 17:16:51 +0200 Subject: [PATCH 4/5] CI: extend goals present tests to check for errors if applicable Extend the goals present tests to additionally check that the response buffer contains some text (i.e., an error message) in those cases where an error is expected. --- ci/simple-tests/coq-test-goals-present.el | 35 +++++++++++++++++------ 1 file changed, 26 insertions(+), 9 deletions(-) diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index e036bd969..98c8faf71 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -141,10 +141,12 @@ BUF should be a string." ;;; define the tests -(defun goals-after-test (coq-src msg) +(defun goals-after-test (coq-src msg check-response-nonempty) "Test that Proof General shows goals after processing COQ-SRC. Process COQ-SRC in a new buffer in one step and check that the -goals buffer is not empty afterwards." +goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY +is non-nil, additionally check that the response buffer is +non-empty, i.e., shows some error message." (message "goals-after-test: Check goals are present after %s." msg) (setq proof-three-window-enable nil) (let (buffer) @@ -161,7 +163,14 @@ goals buffer is not empty afterwards." ;; check that there is a goal in the goals buffer (with-current-buffer "*goals*" (goto-char (point-min)) - (should (looking-at "1 \\(sub\\)?goal (ID")))) + (should (looking-at "1 \\(sub\\)?goal (ID"))) + + (when check-response-nonempty + (message + "goals-after-test: Check response buffer is nonempty after %s." + msg) + (with-current-buffer "*response*" + (should (not (equal (point-min) (point-max))))))) ;; clean up (when buffer @@ -226,24 +235,24 @@ which action the goals buffer should have been reset." (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." - (goals-after-test coq-src-proof "Proof")) + (goals-after-test coq-src-proof "Proof" nil)) (ert-deftest goals-after-comment () "Test goals are present after a comment." - (goals-after-test coq-src-comment "comment")) + (goals-after-test coq-src-comment "comment" nil)) (ert-deftest goals-after-auto () "Test goals are present after ``auto''." - (goals-after-test coq-src-auto "auto")) + (goals-after-test coq-src-auto "auto" nil)) (ert-deftest goals-after-simpl () "Test goals are present after ``simpl''." - (goals-after-test coq-src-simpl "simpl")) + (goals-after-test coq-src-simpl "simpl" nil)) (ert-deftest goals-after-error () "Test goals are present after an error." :expected-result :failed - (goals-after-test coq-src-error "error")) + (goals-after-test coq-src-error "error" t)) (ert-deftest goals-reset-after-admitted () :expected-result :failed @@ -281,6 +290,7 @@ which action the goals buffer should have been reset." ;; (record-buffer-content "*goals*") ;; the complete goal should be present + (message "Check that the complete goal is present in *goals*") (with-current-buffer "*goals*" (goto-char (point-min)) (should (re-search-forward "(eq_one 1 -> False) -> False" nil t))) @@ -293,9 +303,16 @@ which action the goals buffer should have been reset." ;; (record-buffer-content "*goals*") ;; the hypothesis H should be present + (message "Check that the goals buffer has been updated") (with-current-buffer "*goals*" (goto-char (point-min)) - (should (re-search-forward "H : eq_one 1 -> False" nil t)))) + (should (re-search-forward "H : eq_one 1 -> False" nil t))) + + ;; some error should be in the response buffer + (message "Check that there is some error message present") + (with-current-buffer "*response*" + (should (not (equal (point-min) (point-max)))))) + (when buffer (with-current-buffer buffer (set-buffer-modified-p nil)) From 0b42f93d9580b101d1ea83bcd36b289daa605cdf Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 7 Apr 2024 19:20:40 +0200 Subject: [PATCH 5/5] coq: fix goals update after error This commit fixes two more cases of #568: The goals buffer is updated in case of an error if Coq is inside a proof. Care is taken to keep the error message in the response buffer and to show the response buffer in two-pane mode. The fix works by issuing a Show command as a priority action item from proof-shell-handle-error-or-interrupt-hook, which runs at the end of the error processing. The new action item flag 'keep-response tells the generic machinery to not clear the response buffer and to keep it in two-pane mode. --- ci/simple-tests/coq-test-goals-present.el | 2 -- coq/coq.el | 24 +++++++++++++++++++++-- doc/PG-adapting.texi | 1 + generic/pg-goals.el | 17 ++++++++++++---- generic/proof-shell.el | 7 ++++++- 5 files changed, 42 insertions(+), 9 deletions(-) diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index 98c8faf71..d0a3fc0cf 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -251,7 +251,6 @@ which action the goals buffer should have been reset." (ert-deftest goals-after-error () "Test goals are present after an error." - :expected-result :failed (goals-after-test coq-src-error "error" t)) (ert-deftest goals-reset-after-admitted () @@ -272,7 +271,6 @@ which action the goals buffer should have been reset." (ert-deftest update-goals-after-error () "Test goals are updated after an error." - :expected-result :failed (message "update-goals-after-error: Check goals are updated after error") (setq proof-three-window-enable nil) (let (buffer) diff --git a/coq/coq.el b/coq/coq.el index e21ccad27..a6446a174 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -133,7 +133,7 @@ buffer. Sets silent mode. -In normal interaction, the Coq is started because the user assert +In normal interaction, Coq is started because the user assert some commands. Therefore the commands here are followed by those inserted inside `proof-assert-command-hook', respectively, `coq-adapt-printing-width'.") @@ -1874,7 +1874,7 @@ at `proof-assistant-settings-cmds' evaluation time.") (let ((pt2 (point))) (re-search-backward "Goal:\\|^TcDebug\\|^" nil t) (when (looking-at "Goal") - (pg-goals-display (buffer-substring (point) pt2) nil)))))))) + (pg-goals-display (buffer-substring (point) pt2) nil nil)))))))) ;; overwrite the generic one, interactive prompt is Debug mode;; try to display ;; the debug goal in the goals buffer. @@ -3063,6 +3063,26 @@ buffer." (add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t) +(defun coq-show-goals-on-error () + "Update goals buffer on error if necessary. +This function is intended for +`proof-shell-handle-error-or-interrupt-hook'. When Coq reported +an error, this function issues a Show command to update the goals +buffer, in case we are inside a proof. The hook is processed deep +inside `proof-shell-filter' after the action list has been reset +and the proof shell lock `proof-shell-busy' has been released, +all because of the error. The Show must therefore be added as +priority action. The flags of the action item must contain +`'keep-response', because in two-pane mode we want to show the +response buffer to the user." + (when coq-last-but-one-proofstack + (proof-add-to-priority-queue + (proof-shell-action-list-item + "Show. " 'proof-done-invisible + (list 'keep-response 'invisible 'empty-action-list))))) + +(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-show-goals-on-error) + ;; ;; Scroll response buffer to maximize display of first goal ;; diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 37aaaa518..5fb19d655 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3888,6 +3888,7 @@ bother the user. They may include @code{'no-response-display} do not display messages in @strong{response} buffer @code{'no-error-display} do not display errors/take error action @code{'no-goals-display} do not goals in @strong{goals} buffer + @code{'keep-response} do not erase the response buffer when goals are shown @code{'proof-tree-show-subgoal} item inserted by the proof-tree package @code{'priority-action} item added via @code{proof-add-to-priority-queue} @code{'empty-action-list} @code{proof-shell-empty-action-list-command} should not be diff --git a/generic/pg-goals.el b/generic/pg-goals.el index f7cb9b3c7..0bba1553c 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features. ;; ;; Goals buffer processing ;; -(defun pg-goals-display (string keepresponse) +(defun pg-goals-display (string keepresponse nodisplay) "Display STRING in the `proof-goals-buffer', properly marked up. Converts term substructure markup into mouse-highlighted extents. @@ -90,7 +90,13 @@ function tries to do that by calling `pg-response-maybe-erase'. If KEEPRESPONSE is non-nil, we assume that a response message corresponding to this goals message has already been displayed before this goals message (see `proof-shell-handle-delayed-output'), -so the response buffer should not be cleared." +so the response buffer should not be cleared. + +IF NODISPLAY is non-nil, do not display the goals buffer in some +window (but the goals buffer is updated as described above and +any window currently showing it will keep it). In two-pane mode, +NODISPLAY has the effect that the goals are updated but the +response buffer is displayed." ;; Response buffer may be out of date. It may contain (error) ;; messages relating to earlier proof states @@ -114,8 +120,11 @@ so the response buffer should not be cleared." (set-buffer-modified-p nil) ;; Keep point at the start of the buffer. - (proof-display-and-keep-buffer - proof-goals-buffer (point-min)))) + ;; (For Coq, somebody sets point to the conclusion in the goal, so the + ;; position argument in proof-display-and-keep-buffer has no effect.) + (unless nodisplay + (proof-display-and-keep-buffer + proof-goals-buffer (point-min))))) ;; ;; Actions in the goals buffer diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 57d538734..4a97346b5 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -38,6 +38,8 @@ ;; -> proof-shell-process-urgent-message ;; -> proof-shell-filter-manage-output ;; -> proof-shell-handle-immediate-output +;; -> proof-shell-handle-error-or-interrupt +;; -> proof-shell-error-or-interrupt-action ;; -> proof-shell-exec-loop ;; -> proof-tree-check-proof-finish ;; -> proof-shell-handle-error-or-interrupt @@ -113,6 +115,7 @@ bother the user. They may include 'no-response-display do not display messages in *response* buffer 'no-error-display do not display errors/take error action 'no-goals-display do not goals in *goals* buffer + 'keep-response do not erase the response buffer when goals are shown 'proof-tree-show-subgoal item inserted by the proof-tree package 'priority-action item added via proof-add-to-priority-queue 'empty-action-list proof-shell-empty-action-list-command should not be @@ -1818,7 +1821,9 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output both)) + (pg-goals-display proof-shell-last-goals-output + (or both (member 'keep-response flags)) + (member 'keep-response flags))) ;; indicate a goals output has been given 'goals))