prooftree: wait for show-goal commands at proof end

This commit solves the following problem: At the end of a proof
with proof-tree display, a number of show goal requests from
prooftree must possibly be processed, before prooftree sends the
confirm-proof-complete message to signal that Proof General can
continue. For Coq these show goal commands must be sent to Coq
before the dependent evar line is switched off and the result
must be processed by Proof General, therefore before
`proof-tree-external-display' is switched off. Proof General must
therefore stop processing the queue region after the command that
finished the proof until all show goals are processed, the
dependend evar line is off and `proof-tree-external-display' is
nil again. This is achieved by only keeping the priority actions
on proof-action-list and moving whatever remains to
proof-tree--delayed-actions and setting
proof-second-action-list-active. This way only priority actions
(read show goal commands) are processed until prooftree signals
completion and the stuff on proof-tree--delayed-actions is moved
back. To implement this, I introduced (again) an urgent
action (proof-tree-check-proof-finish), which checks for the end
of the proof or the arrival of the last priority action connected
with the current proof-tree display (tagged 'proof-tree-last-item
and queued by the call back proof-tree-confirm-proof-complete).

coq/coq.el

@@ -2031,6 +2031,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-tree-branch-finished-regexp coq-proof-tree-branch-finished-regexp
    proof-tree-show-sequent-command 'coq-show-sequent-command
    proof-tree-find-undo-position 'coq-proof-tree-find-undo-position
+   proof-tree-display-stop-command 'coq-proof-tree-disable-evars
    )
 
   (proof-shell-config-done))
@@ -2228,31 +2229,27 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 ;; display is finished. One such way is to disable the proof tree display
 ;; in the middle of a proof and then to undo a few tactics.
 
-(defun coq-proof-tree-insert-evar-command (cmd)
-  "Insert an evar printing command at the head of `proof-action-list'."
-  (proof-add-to-queue
-   (list
-    (proof-shell-action-list-item
-     (concat cmd " Printing Dependent Evars Line.")
-     'proof-done-invisible
-     (list 'invisible 'no-response-display)))))
+(defun coq-proof-tree-evar-command (cmd)
+  "Return the evar printing command for CMD as action list item."
+  (proof-shell-action-list-item
+   (concat cmd " Printing Dependent Evars Line.")
+   'proof-done-invisible
+   (list 'invisible 'no-response-display)))
 
 (defun coq-proof-tree-enable-evars ()
   "Enable the evar status line for Coq >= 8.6."
   (when (and (coq--post-v86) coq-proof-tree-manage-dependent-evar-line)
     (proof-shell-ready-prover)
-    (coq-proof-tree-insert-evar-command "Set")))
+    (proof-add-to-priority-queue (coq-proof-tree-evar-command "Set"))))
 
 (add-hook 'proof-tree-start-display-hook #'coq-proof-tree-enable-evars)
 
 (defun coq-proof-tree-disable-evars ()
-  "Unconditionally disable evar printing.
-This function switches off evar printing when the proof tree
-display has bee finished (possibly by the end of the proof)."
+  "Return action list item to disable evar printing.
+Function for `proof-tree-display-stop-command'."
+  ;; XXX disable proof tree completely for < 8.10
   (when (and (coq--post-v86) coq-proof-tree-manage-dependent-evar-line)
-    (coq-proof-tree-insert-evar-command "Unset")))
-
-(add-hook 'proof-tree-stop-display-hook #'coq-proof-tree-disable-evars)
+    (coq-proof-tree-evar-command "Unset")))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

generic/proof-shell.el

@@ -1203,6 +1203,11 @@ contains only invisible elements for Prooftree synchronization."
 	;; 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