fix prooftree for Coq/Rocq running completely silent

- Inside the urgent prooftree action, call now the proof assistant
  specific function `proof-tree-assistant-specific-urgent-action'. For
  Coq/Rocq this adds a show command which calls
  `proof-tree-display-goal-callback' in its callback, which processes
  the output and sends appropriate commands to prooftree.
- Move the call of the urgent prooftree action before calling adding
  `proof-shell-empty-action-list-command', such that these last
  actions happen after the show command.
- In `proof-shell-filter-manage-output', save the end of the previous
  command in new variable `proof-shell-old-proof-marker-position' such
  that callbacks running after the next command has been sent to Coq
  can access it. This is used inside
  `proof-tree-display-goal-callback'.
- proof-tree display is now only supported when Coq runs completely
  silent. Supporting it in the other mode should not be too difficult,
  but I don't think it is worth the effort.

Author: hendriktews

CHANGES

@@ -57,7 +57,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     errors on correct code.
 *** Run Coq completely silent to fix #568. If you experience unexpected
     behavior, please report a bug and disable
-    `coq-run-completely-silent' to switch back to old behavior.
+    `coq-run-completely-silent' to switch back to old behavior. Note
+    that external proof tree display is only supported if Coq/Rocq
+    runs completely silent.
 
 
 * Changes of Proof General 4.5 from Proof General 4.4

coq/coq.el

@@ -89,7 +89,8 @@ of commands and switched to verbose before the last command. A
 manual Show command (C-c C-p) is necessary if the last command
 fails to update the goals buffer (e.g., if it is a comment or it
 is not executed because some other command before failed, see
-also bug report #568)."
+also bug report #568). External proof tree display is only
+supported if this option is t."
   :type 'boolean
   :safe 'booleanp
   :group 'coq)
@@ -233,7 +234,7 @@ It is mostly useful in three window mode, see also
   :package-version '(ProofGeneral . "4.2"))
 
 (defcustom coq-proof-tree-ignored-commands-regexp
-  "^\\(\\(Show\\)\\|\\(Locate\\)\\)"
+  "^\\(\\(Show\\)\\|\\(Locate\\)\\|\\(Proof\\)\\)"
   "Regexp for `proof-tree-ignored-commands-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)
@@ -1998,12 +1999,15 @@ at `proof-assistant-settings-cmds' evaluation time.")
     (setq proof-shell-start-silent-cmd "Set Silent."
           proof-shell-stop-silent-cmd "Unset Silent."))
 
-  ;; prooftree config
-  (setq
-   proof-tree-configured (coq--post-v810)
-   proof-tree-get-proof-info 'coq-proof-tree-get-proof-info
-   proof-tree-find-begin-of-unfinished-proof
-     'coq-find-begin-of-unfinished-proof)
+  ;; prooftree config - prooftree is only supported for Coq/Rocq running silent
+  (when coq-run-completely-silent
+    (setq
+     proof-tree-configured (coq--post-v810)
+     proof-tree-get-proof-info 'coq-proof-tree-get-proof-info
+     proof-tree-find-begin-of-unfinished-proof
+       'coq-find-begin-of-unfinished-proof
+     proof-tree-assistant-specific-urgent-action
+       'proof-tree-coq-urgent-action))
 
   ;; proof-omit-proofs config
   (setq
@@ -2330,11 +2334,16 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 ;; in the middle of a proof and then to undo a few tactics.
 
 (defun coq-proof-tree-evar-command (cmd)
-  "Return the evar printing command for CMD as action list item."
+  "Return the evar printing command for CMD as action list item.
+Adds, among others, `'empty-action-list' to flags to avoid that
+`coq-empty-action-list-command' adds a show command because it
+recognizes a change of a printing option. When the user quits the
+proof tree display inside prooftree, then the evar command likely
+runs as single command."
   (proof-shell-action-list-item
    (concat cmd " Printing Dependent Evars Line.")
    'proof-done-invisible
-   (list 'invisible 'no-response-display)))
+   (list 'invisible 'no-response-display 'empty-action-list)))
 
 (defun coq-proof-tree-enable-evars ()
   "Enable the evar status line."
@@ -2354,6 +2363,35 @@ Function for `proof-tree-display-stop-command'."
   (when (and (coq--post-v86) coq-proof-tree-manage-dependent-evar-line)
     (coq-proof-tree-evar-command "Unset")))
 
+(defun proof-tree-coq-urgent-action (last-item)
+  "Insert show-goal commands when running completely silent.
+Coq specific function for `proof-tree-assistant-specific-urgent-action'.
+When running completely silent, insert a show-goal command for commands
+comming from the user. Be careful to not insert show-goal commands for
+show-goal requests from prooftree or for the items inserted by this
+function. LAST-ITEM is the last proof-action item that has just been
+processed. This function is guaranteed to be called at a place where
+`proof-action-list' can be directly manipulated.
+
+When single stepping through a proof, this function inserts a second
+show command, which is inserted before the one from
+`coq-show-goals-inside-proof'. One would of course be enough, but fixing
+this would be difficult."
+  (let ((flags (nth 3 last-item)))
+    (unless (or (memq 'invisible flags)
+                (memq 'proof-tree-show-subgoal flags))
+      (let ((proof-info (coq-proof-tree-get-proof-info)))
+        ;; Ignore retractions, prooftree only needs fresh sequents.
+        (when (and (>= (car proof-info) proof-tree-last-state)
+                   (cadr proof-info))
+          (push
+           (proof-shell-action-list-item
+	    "Show."
+            (lambda (_span)
+              (proof-tree-display-goal-callback last-item proof-info))
+	    '(invisible no-goals-display no-response-display
+                        proof-tree-show-subgoal))
+           proof-action-list))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -3159,7 +3197,7 @@ Do nothing if `coq-run-completely-silent' is disabled."
     (let* ((flags-1 (list 'dont-show-when-silent 'invisible 'empty-action-list))
            (flags (if keep-response (cons 'keep-response flags-1) flags-1)))
       (proof-add-to-priority-queue
-       (proof-shell-action-list-item "Show. " 'proof-done-invisible flags)))))
+       (proof-shell-action-list-item "Show." 'proof-done-invisible flags)))))
 
 (defun coq-show-goals-on-error ()
   "Update goals after error.

doc/PG-adapting.texi

@@ -2675,7 +2675,7 @@ tokens (for example, editing documentation or source code files).
 @chapter Configuring Proof-Tree Visualization
 
 @b{Parts of this section are outdated. Please create an issue at
-github.com/ProofGeneral/Proof General if you have a question for
+github.com/ProofGeneral/PG if you have a question for
 adapting Prooftree for a new proof assistant.}
 
 The proof-tree visualization feature was written with the idea of
@@ -2939,29 +2939,26 @@ Urgent actions are those that must be executed before
 @code{proof-action-list} to the proof assistant. For execution
 speed, the amount of urgent code should be kept small.
 
-@c TEXI DOCSTRING MAGIC: proof-tree-check-proof-finish
-@defun proof-tree-check-proof-finish last-item
-Urgent action to delay processing at proof end.@*
-This function is called from @samp{@code{proof-shell-exec-loop}} after the
-old item has been removed and before the next item from
-@samp{@code{proof-action-list}} is sent to the proof assistant. Of course
-only when the proof-tree display is active. At the end of the
-proof, this function delays items just following the previous
-proof until all show-goal commands from prooftree and the
-@samp{@code{proof-tree-display-stop-command}} (which switches the dependent
-evar line off for Coq) have been processed.
-
-If this function detects the end of the proof, it moves
-non-priority items following in @samp{@code{proof-action-list}} to
-@samp{@code{proof-tree--delayed-actions}} and sets
-@samp{@code{proof-second-action-list-active}}. When later the command from
-@samp{@code{proof-tree-display-stop-command}} is recognized, the items are
-moved back. If no items follow the end of the previous proof,
-@samp{@code{proof-tree-display-stop-command}} is set to t.
+@c TEXI DOCSTRING MAGIC: proof-tree-urgent-action
+@defun proof-tree-urgent-action last-item
+Urgent actions for proof-tree display.@*
+This is the second entry point of the Proof General prooftree support,
+see also @samp{@code{proof-tree-handle-delayed-output}}. Call
+@samp{@code{proof-tree-check-proof-finish}} to delay processing the queue region at
+the end of a proof until all show-goal commands from prooftree have been
+processed. Do also call @samp{@code{proof-tree-assistant-specific-urgent-action}},
+which appropriately inserts show-goal commands if Coq is running
+completely silent. @var{last-item} is the last proof-action item that has just
+been processed.
+
+When the proof-tree display is active, this function is called from
+@samp{@code{proof-shell-exec-loop}} after the old item has been removed and before
+the next item from @samp{@code{proof-action-list}} is sent to the proof assistant.
+At this place @samp{@code{proof-action-list}} can be directly manipulated.
 @end defun
 
 
-The function @code{proof-tree-check-proof-finish} is called at a point
+The function @code{proof-tree-urgent-action} is called at a point
 where it is save to manipulate @code{proof-action-list}. This is
 essential, because @code{proof-tree-urgent-action} inserts goal
 display commands into @code{proof-action-list} when existential
@@ -2976,9 +2973,10 @@ assistant is already busy with the next item from
 @c TEXI DOCSTRING MAGIC: proof-tree-handle-delayed-output
 @defun proof-tree-handle-delayed-output old-proof-marker cmd flags _span
 Process delayed output for prooftree.@*
-This function is the main entry point of the Proof General
-prooftree support.  It examines the delayed output in order to
-take appropriate actions and maintains the internal state.
+This function is the main entry point of the Proof General prooftree
+support, but see also @samp{@code{proof-tree-urgent-action}}. It examines the
+delayed output in order to take appropriate actions and maintains the
+internal state.
 
 The delayed output to handle is in the region
 [@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}].
@@ -3918,7 +3916,7 @@ See also functions @samp{@code{proof-activate-scripting}} and
 
 @c TEXI DOCSTRING MAGIC: proof-marker
 @defvar proof-marker 
-Marker in proof shell buffer pointing to previous command input.
+Marker in proof shell buffer pointing to the end of previous command input.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-action-list
@@ -3957,7 +3955,12 @@ bother the user.  They may include
   @code{'no-error-display}         do not display errors/take error action
   @code{'no-goals-display}         do not goals in @strong{goals} buffer
   @code{'keep-response}            do not erase the response buffer when goals are shown
-  @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package
+  @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package to display
+                            the current or some other goal
+  @code{'proof-tree-last-item}     marks the item that follows the last show-goal
+                            request after a proof finished with proof-tree
+                            display, causes switch back to normal queue region
+                            processing
   @code{'priority-action}          item added via @code{proof-add-to-priority-queue}
   @code{'empty-action-list}        @code{proof-shell-empty-action-list-command} should not be
                             called if this is the last item in the action list
@@ -3971,6 +3974,17 @@ printing hints).
 See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}.
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-shell-old-proof-marker-position
+@defvar proof-shell-old-proof-marker-position 
+Position of end of second last input inside delayed callbacks.@*
+When callbacks of action items are processed, @samp{@code{proof-marker}} has already
+been advanced to the end of the next input that the proof assistant
+processes in parallel with the callback. This variable permits the
+callback to access the end of the input belonging to its action-list
+item and then process the complete output that the proof assistant has
+sent.
+@end defvar
+
 In Proof General 4.2 and earlier it was always the case that all
 items from the queue region were present in
 @code{proof-action-list}. Because of the new parallel background

generic/proof-shell.el

@@ -41,7 +41,7 @@
 ;;            -> proof-shell-handle-error-or-interrupt
 ;;               -> proof-shell-error-or-interrupt-action
 ;;         -> proof-shell-exec-loop
-;;            -> proof-tree-check-proof-finish
+;;            -> proof-tree-urgent-action
 ;;            -> proof-shell-handle-error-or-interrupt
 ;;            -> proof-shell-insert-action-item
 ;;            -> proof-shell-invoke-callback
@@ -64,7 +64,7 @@
 ;; require proof-tree the compiler complains about a recusive
 ;; dependency.
 (declare-function proof-tree-handle-delayed-output "proof-tree"
-		  (old-proof-marker cmd flags span))
+		  (old-proof-marker cmd flags _span))
 ;; without the nil initialization the compiler still warns about this variable
 (defvar proof-tree-external-display)
 
@@ -79,7 +79,7 @@
 ;;
 
 (defvar proof-marker nil
-  "Marker in proof shell buffer pointing to previous command input.")
+  "Marker in proof shell buffer pointing to the end of previous command input.")
 
 (defvar proof-action-list nil
   "The main queue of things to do: spans, commands and actions.
@@ -116,7 +116,12 @@ bother the user.  They may include
   'no-error-display         do not display errors/take error action
   'no-goals-display         do not goals in *goals* buffer
   'keep-response            do not erase the response buffer when goals are shown
-  'proof-tree-show-subgoal  item inserted by the proof-tree package
+  'proof-tree-show-subgoal  item inserted by the proof-tree package to display
+                            the current or some other goal
+  'proof-tree-last-item     marks the item that follows the last show-goal
+                            request after a proof finished with proof-tree
+                            display, causes switch back to normal queue region
+                            processing
   'priority-action          item added via proof-add-to-priority-queue
   'empty-action-list        proof-shell-empty-action-list-command should not be
                             called if this is the last item in the action list
@@ -181,6 +186,15 @@ background compilation finishes.  Then those items are put into
 (defvar proof-shell-last-response-output ""
   "The last displayed response message.")
 
+(defvar proof-shell-old-proof-marker-position nil
+  "Position of end of second last input inside delayed callbacks.
+When callbacks of action items are processed, `proof-marker' has already
+been advanced to the end of the next input that the proof assistant
+processes in parallel with the callback. This variable permits the
+callback to access the end of the input belonging to its action-list
+item and then process the complete output that the proof assistant has
+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.")
@@ -1235,6 +1249,17 @@ contains only invisible elements for Prooftree synchronization."
 	(setq cbitems (cons item
 			    (proof-shell-slurp-comments)))
 
+	;; This is the point where old items have been removed from
+	;; proof-action-list and where the next item has not yet been
+	;; sent to the proof assistant. This is therefore one of the
+	;; few points where it is safe to manipulate
+	;; proof-action-list.
+
+        ;; Call the urgent action of prooftree, if the display is on.
+        ;; This might add or remove stuff to/from `proof-action-list'.
+        (when proof-tree-external-display
+          (proof-tree-urgent-action item))
+
         ;; If proof-action-list is empty after removing the already
         ;; processed actions and the last action was not already
         ;; added by proof-shell-empty-action-list-command (prover
@@ -1252,17 +1277,6 @@ contains only invisible elements for Prooftree synchronization."
             ;; action-list should be empty at this point
             (setq proof-action-list (append extra-items proof-action-list))))
 
-	;; This is the point where old items have been removed from
-	;; proof-action-list and where the next item has not yet been
-	;; sent to the proof assistant. This is therefore one of the
-	;; few points where it is safe to manipulate
-	;; proof-action-list.
-
-        ;; Call the urgent action of prooftree, if the display is on.
-        ;; This might enqueue items in the priority action list.
-        (when proof-tree-external-display
-          (proof-tree-check-proof-finish item))
-
         ;; Add priority actions to the front of proof-action-list.
         ;; Delay adding of priority items until there is no priority
         ;; item at the head of `proof-action-list', such that more
@@ -1722,8 +1736,12 @@ After processing the current output, the last step undertaken
 by the filter is to send the next command from the queue."
   (let ((span  (caar proof-action-list))
 	(cmd   (nth 1 (car proof-action-list)))
-	(flags (nth 3 (car proof-action-list)))
-	(old-proof-marker (marker-position proof-marker)))
+	(flags (nth 3 (car proof-action-list))))
+
+    ;; Save position of end of last input, such that callbacks called
+    ;; inside `proof-shell-exec-loop' and proof-tree delayed output
+    ;; handling can access it.
+    (setq proof-shell-old-proof-marker-position (marker-position proof-marker))
 
     ;; A copy of the last message, verbatim, never modified.
     (setq proof-shell-last-output
@@ -1741,7 +1759,8 @@ by the filter is to send the next command from the queue."
 	(proof-shell-handle-delayed-output))
       ;; send output to the proof tree visualizer
       (if proof-tree-external-display
-	  (proof-tree-handle-delayed-output old-proof-marker cmd flags span)))))
+	  (proof-tree-handle-delayed-output
+           proof-shell-old-proof-marker-position cmd flags span)))))
 
 
 (defsubst proof-shell-display-output-as-response (flags str)