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.

4 files changed, 26 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
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
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b9ac2b3c..78b36ee7 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 ()
@@ -1836,6 +1837,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 c7afe212..1a01147b 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)