From 93a0d1ca16fd30e89e312932008106bc5503386f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 12 Dec 2016 10:05:00 +0100 Subject: fix generic interrupt procedure to interrupt parallel background compilation --- generic/proof-shell.el | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'generic/proof-shell.el') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7a397a06..51038fa6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -464,7 +464,9 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (proc (get-buffer-process (current-buffer))) (bufname (buffer-name))) (message "%s, cleaning up and exiting..." bufname) - (run-hooks 'proof-shell-signal-interrupt-hook) + (let (prover-was-busy) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook)) (redisplay t) (when (and alive proc) @@ -826,14 +828,18 @@ In the first case, PG will terminate the queue of commands at the first available point. In the second case, you may need to press enter inside the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)." (interactive) - (unless (proof-shell-live-buffer) + (let ((prover-was-busy nil)) + (unless (proof-shell-live-buffer) (error "Proof process not started!")) - (unless proof-shell-busy - (error "Proof process not active!")) - (setq proof-shell-interrupt-pending t) - (with-current-buffer proof-shell-buffer - (interrupt-process)) - (run-hooks 'proof-shell-signal-interrupt-hook)) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook) + (if proof-shell-busy + (progn + (setq proof-shell-interrupt-pending t) + (with-current-buffer proof-shell-buffer + (interrupt-process))) + (unless prover-was-busy + (error "Proof process not active!"))))) -- cgit v1.2.3