branch: elpa/proof-general
commit 0d7cca26ebd3efa9dd237ec2a67e836c9f8d1728
Author: Hendrik Tews <hend...@askra.de>
Commit: Hendrik Tews <hend...@askra.de>
fix response display in corner cases
Fix display of the response buffer for display and query commands
generated by Proof General when Coq runs completely silent for the
following corner cases:
- when the response is empty
- in the no more goals state
- when printing all is temporarily switched on for the display/query
command
---
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
