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))

Reply via email to