branch: elpa/proof-general
commit f003572c03404e9786cbdc4797362c425540db68
Author: Hendrik Tews <hend...@askra.de>
Commit: Hendrik Tews <hend...@askra.de>
generic: reset proof-shell-delayed-output-{start,end,flags} regularly
Before this change, proof-shell-delayed-output-{start,end,flags} were
only set inside proof-shell-filter-manage-output but never reset.
Setting these variables happens immediately before the call to
proof-shell-exec-loop, i.e., after processing urgent messages in
proof-shell-process-urgent-messages and after handling errors in
proof-shell-handle-immediate-output. Therefore urgent and error
messages were processed with stale values in
proof-shell-delayed-output-{start,end,flags} that corresponded to the
previous piece of processed output. This resulted at least in the
following odd behavior:
- On error, the previous output was processed again with
proof-shell-handle-delayed-output and the error was often classified
as goals in proof-shell-last-output-kind.
- On error, both proof-shell-handle-delayed-output-hook and
proof-shell-handle-error-or-interrupt-hook were run, resulting in
two calls to coq-show-goals-inside-proof, which in turn usually
resulted in two Show commands after an error for Coq/Rocq, but
sometimes also no Show command, because of the stale flags.
Resetting proof-shell-delayed-output-{start,end,flags} at the begin of
proof-shell-filter fixes these points, even though they have not been
identified as problematic until now.
The correctly running hooks make it possible to fix another
corner-case problem when running silent, see test
error-message-visible-at-qed-complete-script.
---
ci/simple-tests/coq-test-goals-present.el | 3 +--
coq/coq.el | 25 +++++++++++++++----------
doc/PG-adapting.texi | 9 ++++++---
generic/proof-shell.el | 27 ++++++++++++++++++++++++---
4 files changed, 46 insertions(+), 18 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index e26d16f5de..730a57c1ce 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -174,7 +174,7 @@ Used in `check-response-present' for all
`response-buffer-visible-*' tests.")
(* marker A *)
Qed.
"
- "Coq source for ert-deftest error-message-visible-at-proof-end")
+ "Coq source for ert-deftest's error-message-visible-at-qed-*")
;;; utility functions
@@ -490,7 +490,6 @@ variable and check that the error message is displayed."
(kill-buffer buffer)))))
(ert-deftest error-message-visible-at-qed-complete-script ()
- :expected-result :failed
"Check that the error message is present at the end of the proof.
Run a complete script that provokes an error at Qed about a not declared
section variable and check that the error message is displayed."
diff --git a/coq/coq.el b/coq/coq.el
index 375ee0d9d8..7d0f528b76 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3190,7 +3190,7 @@ Important: Coq gives char positions in bytes instead of
chars.
(add-hook 'proof-shell-handle-error-or-interrupt-hook
#'coq-highlight-error-hook t)
-(defun coq-show-goals-inside-proof (keep-response)
+(defun coq-show-goals-inside-proof (keep-response on-error)
"Update goals when action item list has been processed, if running silent.
If `coq-run-completely-silent' is set, add a Show command as
priority action, such that it will still be processed if the
@@ -3203,12 +3203,16 @@ The Show command is only added inside proofs and only
if the last
processed command was not a show command from this function. The
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. 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'.
+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. 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'. ON-ERROR should be set
+when there is some important message in the response buffer. In this
+case `'no-response-display' is added to the flags such that a \"no more
+goals\" reply to the Show command does not overwrite the response
+buffer.
Do nothing if `coq-run-completely-silent' is disabled."
(when (and coq-run-completely-silent
@@ -3216,7 +3220,8 @@ Do nothing if `coq-run-completely-silent' is disabled."
(not (member 'dont-show-when-silent
proof-shell-delayed-output-flags)))
(let* ((flags-1 (list 'dont-show-when-silent 'invisible
'empty-action-list))
- (flags (if keep-response (cons 'keep-response flags-1) flags-1)))
+ (flags-2 (if on-error (cons 'no-response-display flags-1) flags-1))
+ (flags (if keep-response (cons 'keep-response flags-2) flags-2)))
(proof-add-to-priority-queue
(proof-shell-action-list-item "Show." 'proof-done-invisible flags)))))
@@ -3226,7 +3231,7 @@ This function is intended for
`proof-shell-handle-error-or-interrupt-hook' to update the goals
buffer after an error has been detected. See also
`coq-show-goals-inside-proof'."
- (coq-show-goals-inside-proof t))
+ (coq-show-goals-inside-proof t t))
(defun coq-show-goals-standard-case ()
"Update goals after last command when no error was detected.
@@ -3236,7 +3241,7 @@ buffer after the last command has been processed and no
error has
been detected. Take care to keep the response buffer visible if
the last command was a Search, a Check or something similar. See
also `coq-show-goals-inside-proof'."
- (coq-show-goals-inside-proof (eq proof-shell-last-output-kind 'response)))
+ (coq-show-goals-inside-proof (eq proof-shell-last-output-kind 'response)
nil))
(add-hook 'proof-shell-handle-error-or-interrupt-hook
#'coq-show-goals-on-error)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index c7e1097418..05327433c9 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -4289,16 +4289,19 @@ to examine @samp{@code{proof-shell-last-output}}.
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-start
@defvar proof-shell-delayed-output-start
A record of the start of the previous output in the shell buffer.@*
-The previous output is held back for processing at end of queue.
+The previous output is held back for processing at end of queue. Reset
+in @samp{@code{proof-shell-filter}}, i.e., when subsequent output arrives.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-end
@defvar proof-shell-delayed-output-end
A record of the start of the previous output in the shell buffer.@*
-The previous output is held back for processing at end of queue.
+The previous output is held back for processing at end of queue. Reset
+in @samp{@code{proof-shell-filter}}, i.e., when subsequent output arrives.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-flags
@defvar proof-shell-delayed-output-flags
-A copy of the @samp{@code{proof-action-list}} flags for
@samp{proof-shell-delayed-output}.
+A copy of the @samp{@code{proof-action-list}} flags for
@samp{proof-shell-delayed-output}.@*
+Reset in @samp{@code{proof-shell-filter}}, i.e., when subsequent output
arrives.
@end defvar
@vindex proof-action-list
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 8fb609af5d..690b2c3dae 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -40,13 +40,19 @@
;; -> proof-shell-handle-immediate-output
;; -> proof-shell-handle-error-or-interrupt
;; -> proof-shell-error-or-interrupt-action
+;; -> proof-shell-handle-error-or-interrupt-hook
;; -> proof-shell-exec-loop
;; -> proof-tree-urgent-action
;; -> proof-shell-handle-error-or-interrupt
+;; -> proof-shell-error-or-interrupt-action
+;; -> proof-shell-handle-error-or-interrupt-hook
;; -> proof-shell-insert-action-item
;; -> proof-shell-invoke-callback
;; -> proof-release-lock
;; -> proof-shell-handle-delayed-output
+;; -> proof-shell-display-output-as-response
+;; -> pg-goals-display
+;; -> proof-shell-handle-delayed-output-hook
;; -> proof-tree-handle-delayed-output
;; -> proof-release-lock
;; -> proof-start-prover-with-priority-items-maybe
@@ -197,14 +203,17 @@ sent.")
(defvar proof-shell-delayed-output-start nil
"A record of the start of the previous output in the shell buffer.
-The previous output is held back for processing at end of queue.")
+The previous output is held back for processing at end of queue. Reset
+in `proof-shell-filter', i.e., when subsequent output arrives.")
(defvar proof-shell-delayed-output-end nil
"A record of the start of the previous output in the shell buffer.
-The previous output is held back for processing at end of queue.")
+The previous output is held back for processing at end of queue. Reset
+in `proof-shell-filter', i.e., when subsequent output arrives.")
(defvar proof-shell-delayed-output-flags nil
- "A copy of the `proof-action-list' flags for `proof-shell-delayed-output'.")
+ "A copy of the `proof-action-list' flags for `proof-shell-delayed-output'.
+Reset in `proof-shell-filter', i.e., when subsequent output arrives.")
(defvar proof-shell-interrupt-pending nil
"A flag indicating an interrupt is pending.
@@ -787,6 +796,12 @@ didn't cause prover output."
(t ; error
(if proof-shell-delayed-output-start
(save-excursion
+ ;; I don't understand these lines here.
+ ;; `proof-shell-handle-delayed-output' uses
+ ;; `proof-shell-delayed-output-start' and
+ ;; `proof-shell-delayed-output-end', however, I cannot
+ ;; find any code path arriving here where these variables
+ ;; are properly set.
(proof-shell-handle-delayed-output)))
(proof-shell-handle-error-output
(if proof-shell-truncate-before-error proof-shell-error-regexp)
@@ -1606,6 +1621,12 @@ with initializing the process. After that,
`proof-marker'
is only changed when input is sent in `proof-shell-insert'."
(save-excursion
+ ;; Reset delayed output markers and flags. If we find output they
+ ;; will be set again inside `proof-shell-filter-manage-output'.
+ (setq proof-shell-delayed-output-start nil)
+ (setq proof-shell-delayed-output-end nil)
+ (setq proof-shell-delayed-output-flags nil)
+
;; Process urgent messages.
(and proof-shell-eager-annotation-start
(proof-shell-process-urgent-messages))
