From be78d3cb0c0a1c09ff1a279bf84c59b9da059cbc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Wed, 27 May 2020 19:53:05 +0200
Subject: [PATCH] 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              |  2 +-
 generic/proof-config.el | 10 +++++++++-
 generic/proof-script.el |  3 +++
 generic/proof-shell.el  |  1 +
 4 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 71112fc1b..0243f029e 100644
--- a/coq/coq.el
+++ b/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)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 14fcdcac6..b6a1b363c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1771,6 +1771,15 @@ This hook is used within Proof General to refresh the toolbar."
   :type '(repeat function)
   :group 'proof-shell)
 
+
+(defcustom proof-state-change-pre-hook nil
+  "Things to do before proof-done-advancing.
+
+E.g. classify spans by looking at the prompt."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+
 ;;;;;;
 (defcustom proof-dependencies-system-specific nil
   "Set this variable to handle system specific dependency output.
@@ -1787,7 +1796,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 761a3bbe9..a5109be7c 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 a0e80fa70..c9077183c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1833,6 +1833,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