diff options
| author | Pierre Courtieu | 2020-05-27 19:53:05 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-06-04 14:33:10 +0200 |
| commit | 5c3ebac1e8d67f2124d4cbae86134d2a68e2900e (patch) | |
| tree | 8c457ce9ead935f2addcd1c897c994ea83748584 /generic/proof-config.el | |
| parent | 5ba7aee8a8996b8219a6e9dbde645e53684afbca (diff) | |
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.
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 22 |
1 files changed, 20 insertions, 2 deletions
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 |