aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-12-12 10:05:00 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-12-14 21:18:16 +0100
commit93a0d1ca16fd30e89e312932008106bc5503386f (patch)
tree38167b0bd4211654eb783a3771f4c7381b09ba95 /generic
parent43e54c598bbe778e67fe926e770b5235c6745045 (diff)
fix generic interrupt procedure to interrupt parallel background compilation
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el7
-rw-r--r--generic/proof-shell.el22
2 files changed, 20 insertions, 9 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b4898a35..8ce53168 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier
than `proof-shell-handle-error-or-interrupt-hook', which runs
when the interrupt is acknowledged inside `proof-shell-exec-loop'.
-This hook also runs when the proof assistent is killed."
+This hook also runs when the proof assistent is killed.
+
+Hook functions should set the dynamic variable `prover-was-busy'
+to t if there might have been a reason to interrupt. Otherwise
+the generic interrupt handler might issue a prover-not-busy
+error."
:type '(repeat function)
:group 'proof-shell)
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!")))))