branch: elpa/proof-general commit 999cafbe7320ae887f7eebd441beab7e5b0ae6eb Merge: d4d2465d01 f003572c03 Author: hendriktews <hend...@askra.de> Commit: GitHub <nore...@github.com>
Merge pull request #832 from hendriktews/fix-delayed generic: reset proof-shell-delayed-output-{start,end,flags} regularly --- 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))