branch: elpa/proof-general
commit 964a5958e7c8ebdf1bf264342861f6644c34c6cd
Merge: f5d929ec44 0d7cca26eb
Author: hendriktews <hend...@askra.de>
Commit: GitHub <nore...@github.com>
Merge pull request #831 from hendriktews/fix-response
Fix response
---
ci/simple-tests/coq-test-goals-present.el | 5 -----
coq/coq.el | 37 ++++++++++++++++++++++++-------
generic/proof-shell.el | 6 +++++
3 files changed, 35 insertions(+), 13 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index a0c7b1a187..a00e0a0cdb 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -570,7 +570,6 @@ window."
(check-response-present #'coq-Search 6 "(0 <= 2)" "Nat.le_0_2"))
(ert-deftest response-buffer-visible-coq-search-something-proof-end ()
- :expected-result :failed
"Check response for coq-Search on (0 <= 2) at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
@@ -585,13 +584,11 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "(0 <= 2)" "Nat.le_0_2"))
(ert-deftest response-buffer-visible-coq-search-empty-inside-proof ()
- :expected-result :failed
"Check empty response for coq-Search on 42 inside proof"
(message "Check empty response for Search 42 is shown inside proof")
(check-response-present #'coq-Search 6 "42" t))
(ert-deftest response-buffer-visible-coq-search-empty-proof-end ()
- :expected-result :failed
"Check empty response for coq-Search on 42 at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
@@ -606,7 +603,6 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "42" t))
(ert-deftest response-buffer-visible-coq-check-print-all-inside-poof ()
- :expected-result :failed
"Check response for coq-Check on Nat.add_comm inside proof with printing
all."
(message
"Check response for Check Nat.add_comm inside proof with printing all")
@@ -614,7 +610,6 @@ in proof mode with no more goals."
#'(lambda() (coq-Check t)) 6 "Nat.add_comm" "@eq nat (Nat.add n m)"))
(ert-deftest response-buffer-visible-coq-check-print-all-poof-end ()
- :expected-result :failed
"Check response for coq-Check on Nat.add_comm at proof end with printing
all."
(message
"Check response for Check Nat.add_comm at proof end with printing all")
diff --git a/coq/coq.el b/coq/coq.el
index 9c46a6b97a..375ee0d9d8 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -953,13 +953,17 @@ Otherwise propose identifier at point if any."
(defun coq-ask-do (ask do &optional dontguess postformatcmd wait)
- "Ask for an ident and print the corresponding term."
+ "Ask for an ident and print the corresponding term.
+Add `'dont-show-when-silent' to supress show commands when running
+silent."
(let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
(proof-shell-ready-prover)
(setq cmd (coq-guess-or-ask-for-string ask dontguess))
(proof-shell-invisible-command
(format (concat do " %s .") (funcall postform cmd))
- wait)))
+ wait
+ nil
+ 'dont-show-when-silent)))
(defun coq-flag-is-on-p (testcmd)
@@ -968,11 +972,14 @@ Otherwise propose identifier at point if any."
(let ((resp proof-shell-last-response-output))
(string-match "is on\\>" resp)))
-(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd
testcmd)
+(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd
+ testcmd)
"Play commands SETCMD then CMD and then silently UNSETCMD.
The last UNSETCMD is performed with tag 'empty-action-list so that it
does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at
-the time of writing this documentation)."
+the time of writing this documentation). Also add
+`'dont-show-when-silent' everywhere to suppress show commands when
+running silent."
(let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd))
(flag-is-on (and testcmd (coq-flag-is-on-p testcmd))))
;; We put 'empty-action-list tags on all three commands since we don't want
@@ -980,12 +987,23 @@ the time of writing this documentation)."
;; commands.
(unless flag-is-on (proof-shell-invisible-command
(format " %s ." (funcall postform setcmd))
- nil nil 'no-response-display 'empty-action-list))
+ nil
+ nil
+ 'no-response-display
+ 'empty-action-list
+ 'dont-show-when-silent))
(proof-shell-invisible-command
- (format " %s ." (funcall postform cmd)) 'wait nil 'empty-action-list)
+ (format " %s ." (funcall postform cmd))
+ 'wait
+ nil
+ 'empty-action-list 'dont-show-when-silent)
(unless flag-is-on (proof-shell-invisible-command
(format " %s ." (funcall postform unsetcmd))
- 'waitforit nil 'no-response-display
'empty-action-list))))
+ 'waitforit
+ nil
+ 'no-response-display
+ 'empty-action-list
+ 'dont-show-when-silent))))
(defun coq-ask-do-set-unset (ask do setcmd unsetcmd
&optional dontguess postformatcmd _tescmd)
@@ -3187,7 +3205,10 @@ action item flag `'dont-show-when-silent' is used for
the latter.
KEEP-RESPONSE should be set if the last command produced some
error or response that should be kept and shown to the user. If
-set, the flag `'keep-response' is added to the action item.
+set, the flag `'keep-response' is added to the action item. When the
+show command is processed in `proof-shell-handle-delayed-output', the
+flag causes that the response buffer is not cleared and that in 2-pane
+mode the goals are not explicitely shown, see `pg-goals-display'.
Do nothing if `coq-run-completely-silent' is disabled."
(when (and coq-run-completely-silent
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 91b286fcb5..8fb609af5d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1844,6 +1844,12 @@ i.e., 'goals or 'response."
(setq proof-shell-last-goals-output
(buffer-substring-no-properties gstart gend))
+ ;; The intention of `both' in the following seems to be to
+ ;; detect a message before the goal that should go to the
+ ;; response buffer. I doubt this ever worked when
+ ;; `proof-shell-end-goals-regexp' is set, because in this case
+ ;; `rstart' will be greater than `gmark'.
+ ;;
;; FIXME heuristic: 4 allows for annotation in
;; end-goals-regexp [is it needed?]
(setq both
