aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r--generic/proof-shell.el6
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 51038fa6..13da8d98 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -831,7 +831,11 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
(let ((prover-was-busy nil))
(unless (proof-shell-live-buffer)
(error "Proof process not started!"))
- ;; hook functions might set prover-was-busy
+ ;; Hook functions might set prover-was-busy.
+ ;; In case `proof-action-list' is empty and only
+ ;; `proof-second-action-list-active' is t, the hook functions
+ ;; should clear the queue region and release the proof shell lock.
+ ;; `coq-par-user-interrupt' actually does this.
(run-hooks 'proof-shell-signal-interrupt-hook)
(if proof-shell-busy
(progn