From 1f0724813a4eacb59b7a8d8905619c893d12f03b Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 18 Feb 2024 21:45:49 +0100 Subject: [PATCH] proof-tree: protect against internal errors proof-second-action-list-active cannot be used by two packages (i.e., proof-tree and coq-par-compile) simultaneously. Therefore assert it is off when starting a proof-tree display. Also re-initialize proof-tree--delayed-actions, although it should always be reset at the end of a proof-tree display, if everything works as expected. --- generic/proof-tree.el | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 02f762266..148ff3871 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -1182,6 +1182,12 @@ display is switched off." (let ((proof-start (funcall proof-tree-find-begin-of-unfinished-proof))) ;; ensure internal variables are initialized, because otherwise ;; we cannot process undo's after this + (cl-assert (not proof-second-action-list-active) nil + "second action list active on prooftree start") + (when proof-tree--delayed-actions + (lwarn '(proof-tree) :warning + "proof-tree--delayed-actions not empty on prooftree start")) + (setq proof-tree--delayed-actions nil) (proof-tree-ensure-running) (setq proof-tree-current-proof nil) (setq proof-tree-last-state (car (funcall proof-tree-get-proof-info)))