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-script.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-script.el')
| -rw-r--r-- | generic/proof-script.el | 3 |
1 files changed, 3 insertions, 0 deletions
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 |