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.
---
 generic/proof-shell.el | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'generic/proof-shell.el')

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