From 77c3f2eac868f177b73d2aa59b277e40fc48fd0c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 18 Jan 2017 22:05:37 +0100 Subject: split emergency-cleanup to handle interrupts properly (fixes #143) Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors. --- generic/proof-shell.el | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'generic') 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 -- cgit v1.2.3