branch: elpa/proof-general
commit f5d929ec447f3ad9cddba454e7c2dc6ca43cd732
Merge: 2b1fe31698 41d0e20eb5
Author: hendriktews <hend...@askra.de>
Commit: GitHub <nore...@github.com>
Merge pull request #762 from hendriktews/silent-2
Coq: run silently and explicitly Show when necessary - second attempt
---
CHANGES | 5 +
ci/coq-tests.el | 16 +++
ci/simple-tests/coq-test-goals-present.el | 13 +-
coq/coq.el | 227 +++++++++++++++++++++++++-----
doc/PG-adapting.texi | 71 ++++++----
generic/pg-goals.el | 17 ++-
generic/proof-shell.el | 87 ++++++++----
generic/proof-tree.el | 164 ++++++++++++++++-----
8 files changed, 459 insertions(+), 141 deletions(-)
diff --git a/CHANGES b/CHANGES
index c4a719344d..1f5edd937c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,6 +55,11 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
during auto compilation.
*** Fix issues #687 and #688 where the omit-proofs feature causes
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. 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/ci/coq-tests.el b/ci/coq-tests.el
index 65bbdd9705..9ab3cc9cef 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -200,6 +200,8 @@ For example, COMMENT could be (*test-definition*)"
(ert-deftest 020_coq-test-definition ()
+ ;; There are no infomsgr when running silent.
+ :expected-result :failed
"Test *response* output after asserting a Definition."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
@@ -366,6 +368,9 @@ For example, COMMENT could be (*test-definition*)"
(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
+ ;; When running silent, the Show Proof command is issued, but its
+ ;; output is not (yet) kept in the response buffer.
+ :expected-result :failed
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
@@ -392,6 +397,10 @@ For example, COMMENT could be (*test-definition*)"
(ert-deftest 090_coq-test-regression-Fail()
+ ;; When running silent, the message about indeed failing is not
+ ;; shown. One might fix this test by checking that there is no
+ ;; error, which would be shown without Fail.
+ :expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
@@ -413,6 +422,13 @@ For example, COMMENT could be (*test-definition*)"
;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with
message: Tactic failure: Cannot solve this goal.") "*response*")
(ert-deftest 091_coq-test-regression-Fail()
+ ;; XXX What is the difference between this test and
+ ;; 090_coq-test-regression-Fail?
+
+ ;; When running silent, the message about indeed failing is not
+ ;; shown. One might fix this test by checking that there is no
+ ;; error, which would be shown without Fail.
+ :expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index 4642892f09..a0c7b1a187 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -283,17 +283,14 @@ which action the goals buffer should have been reset."
(ert-deftest goals-after-proof ()
"Test goals are present after ``Proof''."
- :expected-result (if coq--post-v87 :failed :passed)
(goals-after-test coq-src-proof "Proof" nil))
(ert-deftest goals-after-comment ()
"Test goals are present after a comment."
- :expected-result :failed
(goals-after-test coq-src-comment "comment" nil))
(ert-deftest goals-after-auto ()
"Test goals are present after ``auto''."
- :expected-result (if coq--post-v87 :failed :passed)
(goals-after-test coq-src-auto "auto" nil))
(ert-deftest goals-after-simpl ()
@@ -302,7 +299,6 @@ which action the goals buffer should have been reset."
(ert-deftest goals-after-error ()
"Test goals are present after an error."
- :expected-result :failed
(goals-after-test coq-src-error "error" t))
(ert-deftest goals-reset-after-admitted ()
@@ -315,7 +311,6 @@ which action the goals buffer should have been reset."
"Lemma a" "no more goals"))
(ert-deftest goals-reset-qed ()
- :expected-result :failed
"The goals buffer is reset after Qed."
(goals-buffer-should-get-reset coq-src-qed
"Proof using" "Qed"))
@@ -381,7 +376,6 @@ two-pane mode."
(ert-deftest goals-up-to-date-at-error ()
"Check that goals are updated before showing the error."
- :expected-result :failed
(update-goals-when-response coq-src-update-goal-after-error
"Lemma foo"
"H : eq_one 1 -> False"
@@ -404,7 +398,6 @@ This test checks several commands inside a proof with a
final
Search command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
- :expected-result :failed
(update-goals-when-response coq-src-update-goal-after-search
"Lemma g"
"2 = 2"
@@ -427,7 +420,6 @@ This test checks several commands inside a proof with a
final
Check command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
- :expected-result :failed
(update-goals-when-response coq-src-update-goal-after-check
"Lemma h"
"3 = 3"
@@ -578,6 +570,7 @@ window."
(check-response-present #'coq-Search 6 "(0 <= 2)" "Nat.le_0_2"))
(ert-deftest response-buffer-visible-coq-search-something-proof-end ()
+ :expected-result :failed
"Check response for coq-Search on (0 <= 2) at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
@@ -592,11 +585,13 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "(0 <= 2)" "Nat.le_0_2"))
(ert-deftest response-buffer-visible-coq-search-empty-inside-proof ()
+ :expected-result :failed
"Check empty response for coq-Search on 42 inside proof"
(message "Check empty response for Search 42 is shown inside proof")
(check-response-present #'coq-Search 6 "42" t))
(ert-deftest response-buffer-visible-coq-search-empty-proof-end ()
+ :expected-result :failed
"Check empty response for coq-Search on 42 at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
@@ -611,6 +606,7 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "42" t))
(ert-deftest response-buffer-visible-coq-check-print-all-inside-poof ()
+ :expected-result :failed
"Check response for coq-Check on Nat.add_comm inside proof with printing
all."
(message
"Check response for Check Nat.add_comm inside proof with printing all")
@@ -618,6 +614,7 @@ in proof mode with no more goals."
#'(lambda() (coq-Check t)) 6 "Nat.add_comm" "@eq nat (Nat.add n m)"))
(ert-deftest response-buffer-visible-coq-check-print-all-poof-end ()
+ :expected-result :failed
"Check response for coq-Check on Nat.add_comm at proof end with printing
all."
(message
"Check response for Check Nat.add_comm at proof end with printing all")
diff --git a/coq/coq.el b/coq/coq.el
index d12382d4a2..9c46a6b97a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -76,6 +76,25 @@
;; :type 'number
;; :group 'coq)
+(defcustom coq-run-completely-silent t
+ "Run Coq completely silent if enabled.
+Please restart Proof General after changing this setting!
+
+If enabled, run Coq completely silent (Set Silent) and only issue
+a show command when necessary to update the goals buffer. This
+behavior is new. If you experience strange effects, please report
+a bug and switch this flag off to return to old behavior. When
+disabled, Coq is dynamically switched to silent for longer lists
+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). External proof tree display is only
+supported if this option is t."
+ :type 'boolean
+ :safe 'booleanp
+ :group 'coq)
+
(defcustom coq-user-init-cmd nil
"User defined init commands for Coq.
These are appended at the end of `coq-shell-init-cmd'."
@@ -122,8 +141,22 @@ Namely, goals that do not fit in the goals window."
;; should re-intialize to coq-search-blacklist-string instead of
;; keeping the current value (that may come from another file).
,(format "Add Search Blacklist %s." coq-search-blacklist-current-string))
- '("Set Suggest Proof Using.") coq-user-init-cmd)
- "Command to initialize the Coq Proof Assistant.")
+ '("Set Suggest Proof Using.")
+ (if coq-run-completely-silent '("Set Silent.") ())
+ coq-user-init-cmd)
+ "Commands for initial Coq configuration, Coq variant of
`proof-shell-init-cmd'.
+List of commands sent to the Coq background process just after it
+has been started. This happens inside `proof-shell-config-done',
+when the major mode `coq-shell-mode' is configured in the `*coq*'
+buffer.
+
+Sets silent mode if `coq-run-completely-silent' is set. Note that
+this constant is not updated when `coq-run-completely-silent' is changed.
+
+In normal interaction, Coq is started because the user asserts
+some commands. Therefore the commands here are followed by those
+inserted inside `proof-assert-command-hook', respectively,
+`coq-adapt-printing-width'.")
;; FIXME: Even if we don't use coq-indent for indentation, we still need it for
;; coq-script-parse-cmdend-forward/backward and coq-find-real-start.
@@ -201,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)
@@ -1206,12 +1239,15 @@ Printing All set."
;; command and *not* have the goal redisplayed, the command must be tagged with
;; 'empty-action-list.
(defun coq-empty-action-list-command (cmd)
- "Return the list of commands to send to Coq after CMD
-if it is the last command of the action list.
-If CMD is tagged with 'empty-action-list then this function won't
-be called and no command will be sent to Coq.
+ "Return the list of commands to send to Coq if CMD is last in the action
list.
+Return the list of commands to be sent to Coq when
+`proof-action-list' is empty, CMD was the last command just sent
+to Coq and CMD was not tagged with `'empty-action-list'.
Note: the last command added if `coq-show-proof-stepwise' is set
-should match the `coq-show-proof-diffs-regexp'."
+should match the `coq-show-proof-diffs-regexp'.
+
+This function is called from `proof-shell-exec-loop' via
+`proof-shell-empty-action-list-command'."
(cond
((or
;; If closing a nested proof, Show the enclosing goal.
@@ -1224,28 +1260,31 @@ should match the `coq-show-proof-diffs-regexp'."
. ,(coq--show-proof-stepwise-cmds)))
((or
- ;; If we go back in the buffer and the number of abort is less than
- ;; the number of nested goals, then Unset Silent and Show the goal
+ ;; If we go back in the buffer and the number of abort is less than the
+ ;; number of nested goals, that is, if we are inside a proof, then Show
+ ;; the goal.
(and (string-match-p "BackTo\\s-" cmd)
(> (length coq-last-but-one-proofstack) coq--retract-naborts)))
- `("Unset Silent."
- ,(if (coq--post-v810) (coq-diffs) "Show.")
- . ,(coq--show-proof-stepwise-cmds)))
+ (append
+ (unless coq-run-completely-silent '("Unset Silent."))
+ (if (coq--post-v810) (list (coq-diffs)) ())
+ (coq--show-proof-stepwise-cmds)))
((or
- ;; If we go back in the buffer and not in the above case, then only Unset
- ;; silent (there is no goal to show). Still, we need to "Set Diffs" again
+ ;; If we go back in the buffer and not in the above case, i.e., outside a
+ ;; proof, then only set the Diffs option.
(string-match-p "BackTo\\s-" cmd))
- (if (coq--post-v810)
- (list "Unset Silent." (coq-diffs) )
- (list "Unset Silent.")))
+ (append
+ (unless coq-run-completely-silent '("Unset Silent."))
+ (if (coq--post-v810) (list (coq-diffs)) ())))
+
((or
;; If starting a proof, Show Proof if need be
(coq-goal-command-str-p cmd)
;; If doing (not closing) a proof, Show Proof if need be
(and (not (string-match-p coq-save-command-regexp-strict cmd))
(> (length coq-last-but-one-proofstack) 0)))
- (coq--show-proof-stepwise-cmds))))
+ (coq--show-proof-stepwise-cmds))))
;; This does not Set Printing Width, it rather tells pg to do that before each
;; command (if necessary)
@@ -1325,7 +1364,9 @@ redisplayed."
(let ((wdth (or width (coq-guess-goal-buffer-at-next-command))))
;; if no available width, or unchanged, do nothing
(when (and wdth (not (equal wdth coq-shell-current-line-width)))
- (proof-shell-invisible-command (format "Set Printing Width %S." (-
wdth 1)) t)
+ (proof-shell-invisible-command
+ (format "Set Printing Width %S." (- wdth 1))
+ t)
(setq coq-shell-current-line-width wdth)
;; Show iff show non nil and some proof is under way
(when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
@@ -1854,7 +1895,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
(let ((pt2 (point)))
(re-search-forward "</prompt>\\|^Debug:\\|^Going to
execute:\\|^TcDebug" nil t)
(goto-char (match-beginning 0))
- (pg-goals-display (buffer-substring pt2 (point)) nil)
+ (pg-goals-display (buffer-substring pt2 (point)) nil nil)
(beginning-of-line)
(pg-response-message (buffer-substring (point) (point-max)))
)))))
@@ -1951,15 +1992,22 @@ at `proof-assistant-settings-cmds' evaluation time.")
;; span menu
(setq proof-script-span-context-menu-extensions #'coq-create-span-menu)
- (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)
+ ;; When proof-shell-start-silent-cmd and proof-shell-stop-silent-cmd stay at
+ ;; their default value nil, the generic code won't switch Coq to silent and
+ ;; noisy at, respectively, the beginning and end of longer asserted regions.
+ (unless coq-run-completely-silent
+ (setq proof-shell-start-silent-cmd "Set Silent."
+ proof-shell-stop-silent-cmd "Unset Silent."))
+
+ ;; 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
@@ -1984,6 +2032,21 @@ at `proof-assistant-settings-cmds' evaluation time.")
)
(defun coq-shell-mode-config ()
+ "Initialization of `coq-shell-mode' that runs in the `*coq*' buffer.
+The interaction buffer with Coq, `*coq*', uses a major mode that
+is derived via `proof-shell-mode' from `scomint-mode'. This
+function runs as the body of `coq-shell-mode' when the `*coq*'
+buffer is initialized, which happens when the Coq background
+process is started. This function intitalizes the Coq
+personalization of Proof General in the interaction buffer with
+Coq. At the end, this function calls `proof-shell-config-done',
+which initializes the Coq session, e.g., by sending
+`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq.
+
+In normal interaction, the proof assistant is started because the
+user assert some commands. Therefore this function runs only
+shortly before `proof-assert-command-hook', respectively,
+`coq-adapt-printing-width'."
(setq
proof-shell-cd-cmd coq-shell-cd
proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\""))
@@ -2271,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."
@@ -2295,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))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -3075,6 +3172,56 @@ 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)
+ "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
+generic machinery inside `proof-shell-filter' believes it has
+processed the last item from the action list. When Coq runs in
+silent mode, we need to update the goals precisely when
+everything else from the action list has been processed.
+
+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.
+
+Do nothing if `coq-run-completely-silent' is disabled."
+ (when (and coq-run-completely-silent
+ coq-last-but-one-proofstack
+ (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)))
+ (proof-add-to-priority-queue
+ (proof-shell-action-list-item "Show." 'proof-done-invisible flags)))))
+
+(defun coq-show-goals-on-error ()
+ "Update goals after error.
+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))
+
+(defun coq-show-goals-standard-case ()
+ "Update goals after last command when no error was detected.
+This function is intended for
+`proof-shell-handle-delayed-output-hook' to update the goals
+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)))
+
+(add-hook 'proof-shell-handle-error-or-interrupt-hook
+ #'coq-show-goals-on-error)
+(add-hook 'proof-shell-handle-delayed-output-hook
+ #'coq-show-goals-standard-case)
+
;;
;; Scroll response buffer to maximize display of first goal
;;
@@ -3162,8 +3309,15 @@ number of hypothesis displayed, without hiding the goal"
(coq-build-subgoals-string nbgoals
nbunfocused)))
minor-mode-alist)))))))
-
-
+(defun coq-clean-goals-outside-proof ()
+ "Clear goals buffer outside proofs.
+This function ensures that the goals buffer is reset after Qed or
+Admitted. This function is for
+`proof-shell-handle-delayed-output-hook'."
+ (when (or (not coq-last-but-one-proofstack)
+ (proof-string-match coq-shell-proof-completed-regexp
+ proof-shell-last-output))
+ (proof-clean-buffer proof-goals-buffer)))
;; This hook must be added before coq-optimise-resp-windows, in order to be
evaluated
@@ -3173,10 +3327,7 @@ number of hypothesis displayed, without hiding the goal"
(add-hook 'proof-shell-handle-delayed-output-hook
#'coq-update-minor-mode-alist)
(add-hook 'proof-shell-handle-delayed-output-hook
- (lambda ()
- (if (proof-string-match coq-shell-proof-completed-regexp
- proof-shell-last-output)
- (proof-clean-buffer proof-goals-buffer))))
+ #'coq-clean-goals-outside-proof)
(add-hook 'proof-shell-handle-delayed-output-hook
(lambda ()
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 5e9a888e11..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
@@ -3956,8 +3954,18 @@ bother the user. They may include
@code{'no-response-display} do not display messages in
@strong{response} buffer
@code{'no-error-display} do not display errors/take error action
@code{'no-goals-display} do not goals in @strong{goals} buffer
- @code{'proof-tree-show-subgoal} item inserted by the proof-tree package
+ @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 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
+ @code{'dont-show-when-silent} Used for commands that should not be
followed by a
+ show command when running silent.
@end lisp
Note that @code{'invisible} does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
@@ -3966,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/pg-goals.el b/generic/pg-goals.el
index f7cb9b3c70..0bba1553ca 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features.
;;
;; Goals buffer processing
;;
-(defun pg-goals-display (string keepresponse)
+(defun pg-goals-display (string keepresponse nodisplay)
"Display STRING in the `proof-goals-buffer', properly marked up.
Converts term substructure markup into mouse-highlighted extents.
@@ -90,7 +90,13 @@ function tries to do that by calling
`pg-response-maybe-erase'.
If KEEPRESPONSE is non-nil, we assume that a response message
corresponding to this goals message has already been displayed
before this goals message (see `proof-shell-handle-delayed-output'),
-so the response buffer should not be cleared."
+so the response buffer should not be cleared.
+
+IF NODISPLAY is non-nil, do not display the goals buffer in some
+window (but the goals buffer is updated as described above and
+any window currently showing it will keep it). In two-pane mode,
+NODISPLAY has the effect that the goals are updated but the
+response buffer is displayed."
;; Response buffer may be out of date. It may contain (error)
;; messages relating to earlier proof states
@@ -114,8 +120,11 @@ so the response buffer should not be cleared."
(set-buffer-modified-p nil)
;; Keep point at the start of the buffer.
- (proof-display-and-keep-buffer
- proof-goals-buffer (point-min))))
+ ;; (For Coq, somebody sets point to the conclusion in the goal, so the
+ ;; position argument in proof-display-and-keep-buffer has no effect.)
+ (unless nodisplay
+ (proof-display-and-keep-buffer
+ proof-goals-buffer (point-min)))))
;;
;; Actions in the goals buffer
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index c99c344ea8..91b286fcb5 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -38,8 +38,10 @@
;; -> proof-shell-process-urgent-message
;; -> proof-shell-filter-manage-output
;; -> proof-shell-handle-immediate-output
+;; -> 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
@@ -62,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)
@@ -77,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.
@@ -113,8 +115,18 @@ bother the user. They may include
'no-response-display do not display messages in *response* buffer
'no-error-display do not display errors/take error action
'no-goals-display do not goals in *goals* buffer
- 'proof-tree-show-subgoal item inserted by the proof-tree package
+ 'keep-response do not erase the response buffer when goals are
shown
+ '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
+ 'dont-show-when-silent Used for commands that should not be followed by a
+ show command when running silent.
Note that 'invisible does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
@@ -174,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.")
@@ -1081,7 +1102,10 @@ being processed."
(unless (eq proof-shell-busy queuemode)
(proof-debug
"proof-append-alist: wrong queuemode detected for busy shell")
- (cl-assert (eq proof-shell-busy queuemode)))))
+ (cl-assert
+ (eq proof-shell-busy queuemode) nil
+ "wrong queuemode in proof-add-to-queue: %s instead expected %s"
+ proof-shell-busy queuemode))))
(let ((nothingthere (null proof-action-list)))
@@ -1226,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
@@ -1243,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
@@ -1713,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
@@ -1727,13 +1755,13 @@ by the filter is to send the next command from the
queue."
(setq proof-shell-delayed-output-start start)
(setq proof-shell-delayed-output-end end)
(setq proof-shell-delayed-output-flags flags)
- (if (proof-shell-exec-loop)
- (setq proof-shell-last-output-kind
- ;; only display result for last output
- (proof-shell-handle-delayed-output)))
+ (when (proof-shell-exec-loop)
+ ;; only display result for last output
+ (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)
@@ -1826,14 +1854,18 @@ i.e., 'goals or 'response."
(buffer-substring-no-properties rstart gmark)))
;; display goals output second so it persists in 2-pane mode
(unless (memq 'no-goals-display flags)
- (pg-goals-display proof-shell-last-goals-output both))
+ (pg-goals-display proof-shell-last-goals-output
+ (or both (member 'keep-response flags))
+ (member 'keep-response flags)))
;; indicate a goals output has been given
- 'goals))
+ (setq proof-shell-last-output-kind 'goals)))
(t
(proof-shell-display-output-as-response flags proof-shell-last-output)
;; indicate that (only) a response output has been given
- 'response))
+ (if (equal proof-shell-last-output "")
+ (setq proof-shell-last-output-kind nil)
+ (setq proof-shell-last-output-kind 'response))))
;; FIXME (CPC 2015-12-31): The documentation of this hook suggests that it
;; only gets run after new output has been displayed, but this isn't true
at
@@ -2004,7 +2036,8 @@ Ordinary output (and error handling) is disabled, and the
result
(proof-shell-invisible-command cmd 'waitforit
nil
'no-response-display
- 'no-error-display)
+ 'no-error-display
+ 'dont-show-when-silent)
proof-shell-last-output)
;;;###autoload
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))
+ )))))
;;
