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.
---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index efa60349..8b9cec69 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -671,7 +671,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)
-- 
cgit v1.2.3