Skip to content

Commit

Permalink
proof-tree: protect against internal errors
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
hendriktews committed Feb 23, 2024
1 parent b96927e commit 1f07248
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions generic/proof-tree.el
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down

0 comments on commit 1f07248

Please sign in to comment.