branch: elpa/proof-general
commit 1a37480857b6408b0c57e655ceb302ce8f884833
Author: Hendrik Tews <[email protected]>
Commit: hendriktews <[email protected]>
coq: clear goals buffer after admitted
Only add the declaration info message to the right regular expression
and generic Proof General will clear the goals buffer. As a side
effect the declaration info message won't show up in the response
buffer any more. Need to change the tests that rely on this.
---
ci/simple-tests/coq-test-goals-present.el | 1 -
ci/simple-tests/coq-test-omit-proofs.el | 24 +++++++++++++++++++-----
coq/coq.el | 16 ++++++++++++++--
generic/proof-shell.el | 1 +
4 files changed, 34 insertions(+), 8 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index 6572a59455..e0784f1bac 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -174,7 +174,6 @@ 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/ci/simple-tests/coq-test-omit-proofs.el
b/ci/simple-tests/coq-test-omit-proofs.el
index d676ab34bc..f2c140bc36 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -92,10 +92,11 @@ 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 "
+ (message "omit-proofs-omit-and-not-omit: Check several omit proofs features")
(setq proof-omit-proofs-option t
proof-three-window-enable nil)
(reset-coq)
@@ -154,10 +155,21 @@ 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 without error.
+ (goto-char (point-max))
+ (should (search-backward "</prompt>" nil t 2))
+ ;; move behind prompt
+ (forward-char 9)
+ (should (looking-at "Admitted\\.\n"))
+ (forward-line 1)
+ ;; There may be an info message about the declaration. The message
+ ;; may be spread over several lines.
+ (when (looking-at "<infomsg>")
+ (should (search-forward "</infomsg>" nil t))
+ (forward-line 1))
+ ;; no other messages or errors before the next prompt
+ (should (looking-at "\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")
@@ -184,6 +196,7 @@ the normal `proof-locked-face'.
The sources for the test contain a local attribute in form of
'#[local]', which has been introduced only in Coq version 8.9."
+ (message "omit-proofs-never-omit-hints: Check omit proofs feature with Hint")
(skip-unless coq--post-v809)
(setq proof-omit-proofs-option t
proof-three-window-enable nil)
@@ -206,6 +219,7 @@ Test that proofs for Let local declarations are never
omitted and
that proofs of theorems following a Let definition are omitted.
This test only checks the faces in the middle of the proof."
+ (message "omit-proofs-never-omit-lets: Check omit proofs feature with Let")
(setq proof-omit-proofs-option t
proof-three-window-enable nil)
(reset-coq)
diff --git a/coq/coq.el b/coq/coq.el
index fa2063f72a..a036acde3d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -145,8 +145,20 @@ Namely, goals that do not fit in the goals window."
;; "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
"*Command of the inferior process to change the directory.")
-(defvar coq-shell-proof-completed-regexp
"No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|Proof\\s-completed";
\\|This subproof is complete
- "*Regular expression indicating that the proof has been completed.")
+(defvar coq-shell-proof-completed-regexp
+ (concat "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|"
+ "Proof\\s-completed\\|"
+ ;; if printing width is small, eg. when running in batch mode,
+ ;; there might be a line break after infomsg
+ "<infomsg>\n?.*\\s-is\\s-declared"
+ ;; \\|This subproof is complete
+ )
+ "*Regular expression indicating that the proof has been completed.
+Coq instance of `proof-shell-clear-goals-regexp'. Used in
+`proof-shell-process-urgent-message' to determine if the goals
+buffer shall be cleaned. Some of the messages recognized here are
+not printed by Coq in silent mode, such that Proof General might
+fail to delete the goals buffer.")
(defvar coq-goal-regexp
"\\(============================\\)\\|\\(\\(?:sub\\)?goal [0-9]+\\)\n")
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a3f8ae39c6..4de85ddf9f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -35,6 +35,7 @@
;; proof-shell-filter-wrapper
;; -> proof-shell-filter
;; -> proof-shell-process-urgent-messages
+;; -> proof-shell-process-urgent-message
;; -> proof-shell-filter-manage-output
;; -> proof-shell-handle-immediate-output
;; -> proof-shell-exec-loop
