From e21c8e665861e618a980f27feedc1d0b9240571e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 26 Aug 2010 23:08:27 +0000
Subject: proof-interrupt-process: make sure works from non-proof shell
 buffers.

---
 generic/proof-shell.el | 10 +++++-----
 1 file 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)))
 
 
 
-- 
cgit v1.2.3