aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-menu.el
diff options
context:
space:
mode:
authorPierre Courtieu2020-05-27 19:53:05 +0200
committerPierre Courtieu2020-06-04 14:33:10 +0200
commit5c3ebac1e8d67f2124d4cbae86134d2a68e2900e (patch)
tree8c457ce9ead935f2addcd1c897c994ea83748584 /generic/proof-menu.el
parent5ba7aee8a8996b8219a6e9dbde645e53684afbca (diff)
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.
Diffstat (limited to 'generic/proof-menu.el')
0 files changed, 0 insertions, 0 deletions