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

(limited to 'easycrypt')

diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
index 67592973..376936f6 100644
--- a/easycrypt/easycrypt-hooks.el
+++ b/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)))
-- 
cgit v1.2.3