branch: elpa/proof-general
commit 41d0e20eb56bed6d473eb36b414bc9f9bb6a3bf7
Author: Hendrik Tews <hend...@askra.de>
Commit: Hendrik Tews <hend...@askra.de>
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.
---
CHANGES | 4 +-
coq/coq.el | 60 ++++++++++++++----
doc/PG-adapting.texi | 66 ++++++++++++--------
generic/proof-shell.el | 55 +++++++++++------
generic/proof-tree.el | 164 +++++++++++++++++++++++++++++++++++++------------
5 files changed, 255 insertions(+), 94 deletions(-)
diff --git a/CHANGES b/CHANGES
index 4198593e46..1f5edd937c 100644
--- a/CHANGES
+++ b/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
diff --git a/coq/coq.el b/coq/coq.el
index e64136b3a0..9c46a6b97a 100644
--- a/coq/coq.el
+++ b/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.
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 66d6eab9ad..c7e1097418 100644
--- a/doc/PG-adapting.texi
+++ b/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
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 19c93b7f14..91b286fcb5 100644
--- a/generic/proof-shell.el
+++ b/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.")
@@ -1236,6 +1250,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
@@ -1253,17 +1278,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
@@ -1723,8 +1737,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
@@ -1742,7 +1760,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)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 148ff38712..e26ab1e6f5 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -45,7 +45,12 @@
;;
;; A fourth problem is that proof-tree display can only work when the
;; prover output is not suppressed (via `proof-full-annotation').
-;; `proof-shell-should-be-silent' takes care of that.
+;; `proof-shell-should-be-silent' takes care of that. For proof
+;; assistants that run completely silent,
+;; `proof-tree-assistant-specific-urgent-action' should be configured
+;; to insert a show-goal command after each command. The callback of
+;; this proof action list item should be
+;; `proof-tree-display-goal-callback'.
;;
;; Earlier versions of prooftree maintained certain data structures
;; twice, one time in prooftree and one time in Proof General. The
@@ -61,7 +66,7 @@
;; priority actions, nevertheless, they can be delayed for quite some
;; time. It might even happen, that the first show goal command for an
;; additionally spawned subgoal arrives at Proof General only after
-;; the proof has been finished. Prooftree can request additinal
+;; the proof has been finished. Prooftree can request additional
;; sequent updates for instantiated existentials only after that first
;; sequent has arrived. Prooftree keeps a tree with the instantiation
;; dependencies of existentials, such that it can immediately issue
@@ -76,11 +81,12 @@
;; evar line must be processed. On the other hand, all show goal
;; commands arriving late for the preceeding proof must be completely
;; processed with proof tree display enabled. To solve that problem,
-;; `proof-tree-check-proof-finish' is called as urgent action inside
-;; `proof-shell-exec-loop', before the next command in the queue
-;; region is sent to the proof assistant. If this urgent action
-;; recognizes a proof end, it moves all non-priority actions from
-;; `proof-action-list' to `proof-tree--delayed-actions' signaling
+;; `proof-tree-check-proof-finish' is called as urgent action via
+;; `proof-tree-urgent-action' inside `proof-shell-exec-loop', before
+;; the next command in the queue region is sent to the proof
+;; assistant. If this urgent action recognizes a proof end, it moves
+;; all non-priority actions from `proof-action-list' to
+;; `proof-tree--delayed-actions' signaling
;; `proof-second-action-list-active'. This effectively stops
;; processing of the queue region. When the end of the proof is
;; processed in the delayed output handling, Proof General sends a
@@ -339,7 +345,18 @@ An action item is a list `(SPAN COMMANDS ACTION
[DISPLAYFLAGS])',
see `proof-action-list'. The action item must not be recognized
as comment by `proof-shell-slurp-comments', that is COMMANDS must
be a nonempty list of strings. The generic prooftree glue code
-will add 'proof-tree-last-item to DISPLAYFLAGS."
+will add 'proof-tree-last-item to DISPLAYFLAGS when necessary."
+ :type 'function
+ :group 'proof-tree-internals)
+
+(defcustom proof-tree-assistant-specific-urgent-action ()
+ "Function to perform proof assistant specific urgent actions.
+If set, this function is called when the last proof-action item has just
+been processed, before the next item is sent to the proof assistant and
+the callback of the last item is processed. It is guaranteed to be
+called at a point at which `proof-action-list' can be directly
+manipulated. If no urgent action is needed, this option should be left
+at nil."
:type 'function
:group 'proof-tree-internals)
@@ -455,7 +472,8 @@ The command from prooftree has the form \"emacs exec:
show-goal
(proof-shell-action-list-item
show-cmd
(proof-tree-make-show-goal-callback proof-name)
- '(no-goals-display no-response-display proof-tree-show-subgoal)))))
+ '(invisible no-goals-display no-response-display
+ dont-show-when-silent proof-tree-show-subgoal)))))
(display-warning
'(proof-general proof-tree)
(format "Malformed prooftree show-goal command") :warning)))
@@ -505,6 +523,37 @@ The command from prooftree has the form \"emacs exec:
show-goal
"Prooftree sent an invalid data length for insert-command"
:warning))))
+(defun proof-tree-send-stop-command-to-prover (last-item-flag)
+ "Add command `proof-tree-display-stop-command' to priority action list.
+This function adds flag `'dont-show-when-silent' to the action
+list item returned by `proof-tree-display-stop-command' and, when
+LAST-ITEM-FLAG is non-nil, also `'proof-tree-last-item'. The
+former flag ensures that no show goals command is inserted after
+`proof-tree-display-stop-command' when the prover runs completely
+silent. The latter flag serves as marker for
+`proof-tree-check-proof-finish' that all requests from prooftree
+have been processed. The resulting action list item is added to
+`proof-priority-action-list'.
+
+This function is called in 4 situations.
+- A proof has been finished and the confirm-proof-complete
+ message arrived from prooftree. Only in this case
+ LAST-ITEM-FLAG must be set.
+- The user stopped the proof tree display inside Proof General.
+- A stop-displaying message arrived, because the user stopped the
+ proof tree display in prooftree.
+- An undo to a point before the current proof stopped the proof
+ tree display."
+ (let* ((stop-cmd (funcall proof-tree-display-stop-command))
+ (flags-1 (cons 'dont-show-when-silent (nth 3 stop-cmd)))
+ (flags-2 (if last-item-flag
+ (cons 'proof-tree-last-item flags-1)
+ flags-1)))
+ ;; an action list item is a list (span commands action [displayflags])
+ (proof-add-to-priority-queue
+ (list (car stop-cmd) (nth 1 stop-cmd) (nth 2 stop-cmd)
+ flags-2))))
+
(defun proof-tree-confirm-proof-complete (data)
"Callback function for confirm-proof-complete messages.
Add command `proof-tree-display-stop-command' with
@@ -512,11 +561,7 @@ Add command `proof-tree-display-stop-command' with
`proof-tree-check-proof-finish' eventually sees this last command
and switches the proof-tree display processing off."
(if (string-match proof-tree--confirm-complete-regexp data)
- (let ((stop-cmd (funcall proof-tree-display-stop-command)))
- ;; an action list item is a list (span commands action [displayflags])
- (proof-add-to-priority-queue
- (list (car stop-cmd) (nth 1 stop-cmd) (nth 2 stop-cmd)
- (cons 'proof-tree-last-item (nth 3 stop-cmd)))))
+ (proof-tree-send-stop-command-to-prover t)
(display-warning
'(proof-general proof-tree)
"Malformed prooftree confirm-proof-complete command" :error)))
@@ -814,20 +859,22 @@ lambda expressions that you can put into
`proof-action-list'."
`(lambda (_span) (proof-tree-show-goal-callback ,proof-name)))
(defun proof-tree-quit-proof ()
- "Switch proof-tree display handling off inside Proof General."
+ "Switch proof-tree display handling off inside Proof General.
+This function is for stopping the proof-tree display because of
+some user request, which may either be an undo before the start
+of the proof or some kind of quitting the proof-tree display in
+Proof General or in prooftree. In these cases no show-goal
+commands need to be processed, therefore do not add the
+`'proof-tree-last-item' flag to the stop command."
(setq proof-tree-current-proof nil)
- (proof-add-to-priority-queue (funcall proof-tree-display-stop-command)))
+ (proof-tree-send-stop-command-to-prover nil))
(defun proof-tree-check-proof-finish (last-item)
- "Urgent action to delay processing at proof end.
-This function is called from `proof-shell-exec-loop' after the
-old item has been removed and before the next item from
-`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
-`proof-tree-display-stop-command' (which switches the dependent
-evar line off for Coq) have been processed.
+ "Delay queue region at proof end until all show-goal requests are processed.
+At the end of the proof, this function delays items just following the
+previous proof until all show-goal commands from prooftree and the
+`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 `proof-action-list' to
@@ -835,9 +882,7 @@ non-priority items following in `proof-action-list' to
`proof-second-action-list-active'. When later the command from
`proof-tree-display-stop-command' is recognized, the items are
moved back. If no items follow the end of the previous proof,
-`proof-tree-display-stop-command' is set to t."
- (cl-assert proof-tree-external-display nil
- "proof-tree-check-proof-finish precondition failure")
+`proof-tree--delayed-actions' is set to t."
;; (message "PTCPF pt %s current %s mode %s delayed %s item %s"
;; proof-tree-current-proof (cadr (funcall
proof-tree-get-proof-info))
;; proof-shell-busy proof-tree--delayed-actions
@@ -873,6 +918,27 @@ moved back. If no items follow the end of the previous
proof,
(setq proof-tree-current-proof nil)
(setq proof-tree-external-display nil))))
+(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 `proof-tree-handle-delayed-output'. Call
+`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 `proof-tree-assistant-specific-urgent-action',
+which appropriately inserts show-goal commands if Coq is running
+completely silent. 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
+`proof-shell-exec-loop' after the old item has been removed and before
+the next item from `proof-action-list' is sent to the proof assistant.
+At this place `proof-action-list' can be directly manipulated."
+ (cl-assert proof-tree-external-display nil
+ "proof-tree-urgent-action precondition failure")
+ (when proof-tree-assistant-specific-urgent-action
+ (funcall proof-tree-assistant-specific-urgent-action last-item))
+ (proof-tree-check-proof-finish last-item))
+
(defun proof-tree-extract-goals (start end)
"Extract the current goal state information from the delayed output.
If there is a current goal, return a list containing (in
@@ -985,7 +1051,8 @@ The delayed output of the navigation command is in the
region
(defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info)
"Display current goal in prooftree unless CMD should be ignored."
- ;; (message "PTHPC")
+ ;; (message "PTHPC old marker %s cmd |%s| info %s"
+ ;; old-proof-marker cmd proof-info)
(let (;; (proof-state (car proof-info))
(cmd-string (mapconcat #'identity cmd " ")))
(unless (and proof-tree-ignored-commands-regexp
@@ -999,6 +1066,20 @@ The delayed output of the navigation command is in the
region
cmd-string proof-info)))
(setq proof-tree-last-state (car proof-info))))
+(defun proof-tree-display-goal-callback (old-item old-proof-info)
+ "Callback to process a goal for prooftree.
+This function should be used as callback for show-goal commands inserted
+by `proof-tree-assistant-specific-urgent-action' for proof assistants
+running completely silent. OLD-ITEM should be the proof action list item
+for which `proof-tree-assistant-specific-urgent-action' produced a show
+goal command. OLD-PROOF-INFO must be the result of
+`proof-tree-get-proof-info' just after old-item has been processed."
+ ;; (message "PTDGC %s %s" old-item old-proof-info)
+ (with-current-buffer proof-shell-buffer
+ (proof-tree-handle-proof-command proof-shell-old-proof-marker-position
+ (nth 1 old-item)
+ old-proof-info)))
+
(defun proof-tree-handle-undo (proof-info)
"Undo prooftree to current state."
;; (message "PTHU info %s" proof-info)
@@ -1053,9 +1134,10 @@ The delayed output is in the region
(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 `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
\[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
@@ -1100,12 +1182,18 @@ the flags and SPAN is the span."
;; try to keep consistency nevertheless
(setq proof-tree-current-proof current-proof-name)))
- ;; send stuff to prooftree now
- (when current-proof-name
- ;; we are inside a proof: display something
- (proof-tree-ensure-running)
- (proof-tree-handle-proof-command old-proof-marker
- cmd proof-info)))))))
+ ;; This piece of code processes goal output for proof
+ ;; assistants that are not running completetly silent and
+ ;; sends appropriate commands to prooftree. This is not
+ ;; needed now, because Coq/Rocq is running completely
+ ;; silent.
+ ;;
+ ;; (when current-proof-name
+ ;; ;; we are inside a proof: display something
+ ;; (proof-tree-ensure-running)
+ ;; (proof-tree-handle-proof-command old-proof-marker
+ ;; cmd proof-info))
+ )))))
;;
