branch: elpa/proof-general
commit f87fdda64a30c60ead3620f5447279ab544169cb
Author: Hendrik Tews <hend...@askra.de>
Commit: Hendrik Tews <hend...@askra.de>
clear goals buffer after Qed and Admitted when running silent
This solves the remaining known problems from #568. Fixes #568.
---
ci/simple-tests/coq-test-goals-present.el | 2 --
coq/coq.el | 16 ++++++++++------
2 files changed, 10 insertions(+), 8 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index f0d59e73f9..a0c7b1a187 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -303,7 +303,6 @@ which action the goals buffer should have been reset."
(ert-deftest goals-reset-after-admitted ()
"The goals buffer is reset after an Admitted."
- :expected-result :failed
(goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted"))
(ert-deftest goals-reset-no-more-goals ()
@@ -312,7 +311,6 @@ which action the goals buffer should have been reset."
"Lemma a" "no more goals"))
(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"))
diff --git a/coq/coq.el b/coq/coq.el
index 677c31ac1b..e58cc60d7e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3246,8 +3246,15 @@ number of hypothesis displayed, without hiding the goal"
(coq-build-subgoals-string nbgoals
nbunfocused)))
minor-mode-alist)))))))
-
-
+(defun coq-clean-goals-outside-proof ()
+ "Clear goals buffer outside proofs.
+This function ensures that the goals buffer is reset after Qed or
+Admitted. This function is for
+`proof-shell-handle-delayed-output-hook'."
+ (when (or (not coq-last-but-one-proofstack)
+ (proof-string-match coq-shell-proof-completed-regexp
+ proof-shell-last-output))
+ (proof-clean-buffer proof-goals-buffer)))
;; This hook must be added before coq-optimise-resp-windows, in order to be
evaluated
@@ -3257,10 +3264,7 @@ number of hypothesis displayed, without hiding the goal"
(add-hook 'proof-shell-handle-delayed-output-hook
#'coq-update-minor-mode-alist)
(add-hook 'proof-shell-handle-delayed-output-hook
- (lambda ()
- (if (proof-string-match coq-shell-proof-completed-regexp
- proof-shell-last-output)
- (proof-clean-buffer proof-goals-buffer))))
+ #'coq-clean-goals-outside-proof)
(add-hook 'proof-shell-handle-delayed-output-hook
(lambda ()
