From 5c3ebac1e8d67f2124d4cbae86134d2a68e2900e Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 27 May 2020 19:53:05 +0200
Subject: 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.
---
 doc/PG-adapting.texi | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3