From 27d59628a66e393ce9886680fdb231ab51a61dd7 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 27 May 2020 19:53:05 +0200 Subject: [PATCH] New hook for early prompt/output analyzis. proof-state-change-pre-hook happens earlier than proof-state-change-hook, i.e. before proof-done-advancing. This should be used to register information in the currently processed span before proof-done-advancing classifies it. Historically PG design was to gather these information during proof-done-advancing (or in its hook called at the end) by just looking at the command statement. But it is often useful to look at the output (messages and/or prompt) to gather more accurate information. Some of this information may be needed DURING proof-done-advancing. Hence this early hook. --- coq/coq.el | 2 +- doc/PG-adapting.texi | 8 +++++--- easycrypt/easycrypt-hooks.el | 2 +- generic/proof-config.el | 22 ++++++++++++++++++++-- generic/proof-script.el | 3 +++ generic/proof-shell.el | 2 ++ generic/proof-tree.el | 1 + 7 files changed, 33 insertions(+), 7 deletions(-) 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/doc/PG-adapting.texi b/doc/PG-adapting.texi index 5740faa20..14fe5219e 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 675929739..376936f61 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 14fcdcac6..721f42761 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1761,16 +1761,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. @@ -1787,7 +1806,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..7980e0c2a 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 () @@ -1833,6 +1834,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 c7afe2128..1a01147b7 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)