From bf1b876083a3589c2a807a3280abd8a4b7998868 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sun, 3 Mar 2024 21:34:16 +0100
Subject: [PATCH] fix tests for preceding commit

- update manuals
- fix test omit-proofs-omit-and-not-omit: do not use the *response*
  buffer any more
- 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-omit-proofs.el | 15 ++++++++++-----
 doc/PG-adapting.texi                    |  2 ++
 3 files changed, 25 insertions(+), 5 deletions(-)

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-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el
index d676ab34b..8bea2f0d4 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -92,7 +92,7 @@ configured there may be taken from faces with less priority."
   "Test the omit proofs feature.
 In particular, test that with proof-omit-proofs-option configured:
 - the proof _is_ processed when using a prefix argument
-- in this case the proof as normal locked color
+- in this case the proof has normal locked color
 - without prefix arg, the proof is omitted
 - the proof has omitted color then
 - stuff before the proof still has normal color "
@@ -154,10 +154,15 @@ In particular, test that with proof-omit-proofs-option configured:
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (with-current-buffer "*response*"
-    (goto-char (point-min))
-    ;; There should be a declared message.
-    (should (looking-at "classic_excluded_middle is declared")))
+  (with-current-buffer "*coq*"
+    ;; There should be an Admit at the second last prompt.
+    (goto-char (point-max))
+    (should (search-backward "</prompt>" nil t 2))
+    ;; move behind prompt
+    (forward-char 9)
+    ;; There should be a Qed with no error or message after it
+    (should
+     (looking-at "Admitted\\.\n\n<prompt>Coq <")))
 
   ;; Check 4: check proof-omitted-proof-face is active at marker 3
   (message "4: check proof-omitted-proof-face is active at marker 3")
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.,