diff options
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 8 | ||||
| -rw-r--r-- | easycrypt/easycrypt-hooks.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 22 | ||||
| -rw-r--r-- | generic/proof-script.el | 3 | ||||
| -rw-r--r-- | generic/proof-shell.el | 2 | ||||
| -rw-r--r-- | generic/proof-tree.el | 1 |
7 files changed, 33 insertions, 7 deletions
@@ -671,7 +671,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/doc/PG-adapting.texi b/doc/PG-adapting.texi index 5740faa2..14fe5219 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3107,7 +3107,8 @@ before and after sending the command. In case @var{cmd} is (or yields) nil, do nothing. @var{invisiblecallback} will be invoked after the command has finished, -if it is set. It should probably run the hook variables +if it is set. It should probably run the hook variables +@samp{@code{proof-state-change-pre-hook}} and @samp{@code{proof-state-change-hook}}. @var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}. @@ -4056,8 +4057,9 @@ not need to use these directly. @c TEXI DOCSTRING MAGIC: proof-grab-lock @defun proof-grab-lock &optional queuemode Grab the proof shell lock, starting the proof assistant if need be.@* -Runs @samp{@code{proof-state-change-hook}} to notify state change. -If @var{queuemode} is supplied, set the lock to that value. +Runs @samp{@code{proof-state-change-pre-hook}} and +@samp{@code{proof-state-change-hook}} to notify state change. If +@var{queuemode} is supplied, set the lock to that value. @end defun @c TEXI DOCSTRING MAGIC: proof-release-lock diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el index 67592973..376936f6 100644 --- a/easycrypt/easycrypt-hooks.el +++ b/easycrypt/easycrypt-hooks.el @@ -68,7 +68,7 @@ (setq easycrypt-proof-weak-mode (car (cdr infos))) ))) -(add-hook 'proof-state-change-hook 'easycrypt-set-state-infos) +(add-hook 'proof-state-change-pre-hook 'easycrypt-set-state-infos) (defun easycrypt-find-and-forget (span) (let ((span-staten (easycrypt-get-span-statenum span))) diff --git a/generic/proof-config.el b/generic/proof-config.el index 9d352548..6f1e9148 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1766,16 +1766,35 @@ symbol is 'systemspecific." :type '(repeat function) :group 'proof-shell) + +(defcustom proof-state-change-pre-hook nil + "This hook is called when a scripting state change may have occurred. +Specifically, this hook is called after a region has been asserted or +retracted, or after a command has been sent to the prover with +`proof-shell-invisible-command'. + +It is run *before* the generic processing of the command span is +done (see function `prof-done-advancing'). See +`proof-state-change-hook' to insert actions after it." + :type '(repeat function) + :group 'proof-shell) + (defcustom proof-state-change-hook nil "This hook is called when a scripting state change may have occurred. Specifically, this hook is called after a region has been asserted or retracted, or after a command has been sent to the prover with `proof-shell-invisible-command'. -This hook is used within Proof General to refresh the toolbar." +It is run *after* the generic processing of the command span is +done (see function `prof-done-advancing'). See +`proof-state-change-pre-hook' to insert actions before it. + +This hook may be used to refresh the toolbar." :type '(repeat function) :group 'proof-shell) + + ;;;;;; (defcustom proof-dependencies-system-specific nil "Set this variable to handle system specific dependency output. @@ -1792,7 +1811,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 761a3bbe..a5109be7 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 b9ac2b3c..78b36ee7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -243,6 +243,7 @@ If QUEUEMODE is supplied, set the lock to that value." (setq proof-shell-interrupt-pending nil proof-shell-busy (or queuemode t) proof-shell-last-queuemode proof-shell-busy) + (run-hooks 'proof-state-change-pre-hook) (run-hooks 'proof-state-change-hook)) (defun proof-release-lock () @@ -1836,6 +1837,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 diff --git a/generic/proof-tree.el b/generic/proof-tree.el index c7afe212..1a01147b 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -814,6 +814,7 @@ call `proof-tree-make-show-goal-callback', which evaluates to a lambda expressions that you can put into `proof-action-list'." ;;(message "PTSGC %s" state) (proof-tree-update-sequent state) + (run-hooks 'proof-state-change-pre-hook) (run-hooks 'proof-state-change-hook)) (defun proof-tree-make-show-goal-callback (state) |