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

@@ -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)

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

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)))

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

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

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

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)