diff options
| author | David Aspinall | 2010-08-26 23:08:27 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-26 23:08:27 +0000 |
| commit | e21c8e665861e618a980f27feedc1d0b9240571e (patch) | |
| tree | c9cf5e35fae19d82c9d7c9cb82b0b6f7174a7493 | |
| parent | 2b6176e2d3c7d907f29e3b4c59e843b75c068840 (diff) | |
proof-interrupt-process: make sure works from non-proof shell buffers.
| -rw-r--r-- | generic/proof-shell.el | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index e80bdf0b..c47dedee 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -484,10 +484,9 @@ so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Lego and Coq)." (interactive) - (if proof-shell-busy - (progn - (proof-interrupt-process) - (proof-shell-wait))) + (when proof-shell-busy + (proof-interrupt-process) + (proof-shell-wait)) (if (not (proof-shell-live-buffer)) (proof-shell-start) ;; start if not running ;; otherwise clear context @@ -717,7 +716,8 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*). (unless proof-shell-busy (error "Proof process not active!")) (setq proof-shell-interrupt-pending t) - (interrupt-process)) + (with-current-buffer proof-shell-buffer + (interrupt-process))) |