diff --git a/coq/coq.el b/coq/coq.el index 71112fc1b..0243f029e 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -661,7 +661,7 @@ If locked span already has a state number, then do nothing. Also updates ;; This hook seems the one we want. ;; WARNING! It is applied once after each command PLUS once before a group of ;; commands is started -(add-hook 'proof-state-change-hook #'coq-set-state-infos) +(add-hook 'proof-state-change-pre-hook #'coq-set-state-infos) (defun count-not-intersection (l notin) diff --git a/generic/proof-config.el b/generic/proof-config.el index 14fcdcac6..b6a1b363c 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1771,6 +1771,15 @@ This hook is used within Proof General to refresh the toolbar." :type '(repeat function) :group 'proof-shell) + +(defcustom proof-state-change-pre-hook nil + "Things to do before proof-done-advancing. + +E.g. classify spans by looking at the prompt." + :type '(repeat function) + :group 'proof-shell) + + ;;;;;; (defcustom proof-dependencies-system-specific nil "Set this variable to handle system specific dependency output. @@ -1787,7 +1796,6 @@ same type as `proof-dependency-in-span-context-menu' returns." :type '(repeat function) :group 'proof-shell) ;;;;; - (defcustom proof-shell-syntax-table-entries nil "List of syntax table entries for proof script mode. A flat list of the form diff --git a/generic/proof-script.el b/generic/proof-script.el index 761a3bbe9..a5109be7c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1382,6 +1382,8 @@ Argument SPAN has just been processed." (if (span-live-p proof-queue-span) (proof-set-queue-start end)) + (run-hooks 'proof-state-change-pre-hook) + (cond ;; CASE 1: Comments just get highlighted ((eq (span-property span 'type) 'comment) @@ -2120,6 +2122,7 @@ which is true for some proof assistants (but probably not others)." (span-delete span) (if killfn (funcall killfn start end)))) ;; State of scripting may have changed now + (run-hooks 'proof-state-change-pre-hook) (run-hooks 'proof-state-change-hook)) (defun proof-setup-retract-action (start end proof-commands remove-action &optional diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a0e80fa70..192855ae4 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -92,6 +92,22 @@ printing hints). See the functions `proof-start-queue' and `proof-shell-exec-loop'.") +(defvar proof-priority-action-list nil + "Holds action items to be inserted at the head of `proof-action-list' ASAP. +When the proof assistant is busy, one cannot push to the head of +`proof-action-list`, because the head usually (but not always) +contains the item that the proof assistant is currently +executing. This list therefore holds the items to be executed +before any other items in `proof-action-list'. Inside +`proof-shell-exec-loop', when `proof-action-list' is in the right +state, the content of this list if prepended to +`proof-action-list'. Use `proof-add-to-priority-queue' to add +items to this priority list, to ensure the proof assistant starts +running, in case `proof-action-list' is currently empty. + +The items in this list are reversed, that is, the one added last +and to be executed last is at the head.") + (defsubst proof-shell-invoke-callback (listitem) "From `proof-action-list' LISTITEM, invoke the callback on the span." (condition-case err @@ -1062,6 +1078,32 @@ being processed." ;; nothing to do: maybe we completed a list of comments without sending them (proof-detach-queue))))) +(defun start-prover-with-priority-items-maybe () + "Start processing priority items if necessary. +If there are priority items and the proof shell is not busy with +other items, then this function starts the prover with the +priority items. This function relies on the invariants of +`proof-shell-filter-active' and on `proof-action-list'. The +latter is non-empty, if there is some item, which has not been +fully processed yet. + +Note that inside `proof-shell-exec-loop' the priority items are +processed without calling this function." + (when (and proof-priority-action-list + (null proof-action-list) (not proof-shell-filter-active)) + ;; not sure how fast we end up in proof-shell-exec-loop, better to clear + ;; proof-priority-action-list here before calling proof-add-to-queue + (let ((copy proof-priority-action-list)) + (setq proof-priority-action-list nil) + (proof-add-to-queue (nreverse copy))))) + +(defun proof-add-to-priority-queue (queueitem) + "Add item to `proof-priority-action-list' and start the queue if necessary. +Argument QUEUEITEM must be an action item as documented for +`proof-action-list'." + (push queueitem proof-priority-action-list) + (start-prover-with-priority-items-maybe)) + ;;;###autoload (defun proof-start-queue (start end queueitems &optional queuemode) @@ -1158,6 +1200,13 @@ contains only invisible elements for Prooftree synchronization." (if proof-tree-external-display (proof-tree-urgent-action flags)) + ;; add priority actions to the front of proof-action-list + (when proof-priority-action-list + (setq proof-action-list + (nconc (nreverse proof-priority-action-list) + proof-action-list)) + (setq proof-priority-action-list nil)) + ;; if action list is (nearly) empty, ensure prover is noisy. (if (and proof-shell-silent (not (eq (nth 2 item) 'proof-shell-clear-silent)) @@ -1387,7 +1436,7 @@ to `proof-register-possibly-new-processed-file'." "Wrapper for `proof-shell-filter', protecting against parallel calls. In Emacs a process filter function can be called while the same filter is currently running for the same process, for instance, -when the filter bocks on I/O. This wrapper protects the main +when the filter blocks on I/O. This wrapper protects the main entry point, `proof-shell-filter' against such parallel, overlapping calls. @@ -1412,7 +1461,10 @@ calls." (setq proof-shell-filter-active nil proof-shell-filter-was-blocked nil) (signal (car err) (cdr err)))) - (setq call-proof-shell-filter proof-shell-filter-was-blocked))))) + (setq call-proof-shell-filter proof-shell-filter-was-blocked))) + ;; finally leaving proof-shell-filter - maybe somebody has added + ;; priority items inside proof-shell-filter? + (start-prover-with-priority-items-maybe))) (defun proof-shell-filter () @@ -1608,8 +1660,41 @@ by the filter is to send the next command from the queue." (buffer-substring-no-properties start end)) ;; sets proof-shell-last-output-kind + ;;; NB This will remove the span (and all following queued spans) + ;;; if an error occured. So don't use it in the following unless + ;;; you know the command was processed without error. (proof-shell-handle-immediate-output cmd start end flags) + ;; insert a show proof command to have an up-to-date goals buffer + ;; in case of error. Currently PG makes coq silent when proccesing + ;; a bunch of commands, and goes back to unsilent before the last + ;; command. Therefore if an error interrupts a bunch we are still + ;; in silent mode and the goal is not diplayed. The following + ;; inserts a show proof command to have an up-to-date goals buffer + ;; in case of error AND we are in a proof. We don't issue the show + ;; command in other cases as it would be redundant or wrong. + + ;; NB: If we switch to "all silent, ask for show" protocol, then + ;; this would need to be generalized, but maybe not here. + + ;; NB: To avoid looping on errors (like if the printing of the + ;; goal is not possible) these actions are tagged with the flag + ;; 'empty-action-list and trigger the following only if its this + ;; flag is missing. + (when (and (not (memq 'empty-action-list flags)) + (funcall proof-shell-last-cmd-left-goals-p) + (eq proof-shell-last-output-kind 'error)) + ;; to make the error message stay, we need to send a Show + ;; command without updating any buffer and then use the + ;; pg-goals-display can insert the output in goals buffer + ;; without changing the response buffer. + (let ((callback '(lambda (dummyspan);do not use the span, it is probably deleted + (pg-goals-display proof-shell-last-output t)))) + (proof-add-to-priority-queue + (proof-shell-action-list-item + proof-showproof-command callback ;'proof-done-invisible + (list 'no-goals-display 'invisible 'empty-action-list))))) + (unless proof-shell-last-output-kind ; dealt with already (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) @@ -1833,6 +1918,7 @@ If TIMEOUTSECS is a number, time out after that many seconds." (defun proof-done-invisible (span) "Callback for ‘proof-shell-invisible-command’. Call ‘proof-state-change-hook’." + (run-hooks 'proof-state-change-pre-hook) (run-hooks 'proof-state-change-hook)) ;;;###autoload