From ab0e63f2e8ac5f62a8a4bb92f0d8f9df49f1530d Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 10 Mar 2020 22:44:48 +0100 Subject: [PATCH] add proof-priority-action-list new, generic interface for priority action items, see proof-priority-action-list and proof-add-to-priority-queue, for asynchronously adding commands to the head of proof-action-list --- generic/proof-shell.el | 57 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 55 insertions(+), 2 deletions(-) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c9077183c..5f42229c1 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,33 @@ 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'." + (message "PATPQ") + (push queueitem proof-priority-action-list) + (start-prover-with-priority-items-maybe)) + ;;;###autoload (defun proof-start-queue (start end queueitems &optional queuemode) @@ -1158,6 +1201,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 +1437,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 +1462,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 ()