From 8f23b61efea192d249f82c57f15f7fe966850f9a Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 25 Aug 2010 11:11:18 +0000
Subject: proof-retract-before-change: now interrupts are robust in Isabelle,
 try interrupting if prover is busy before undoing.  Refs Trac #293

---
 generic/proof-script.el | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 069b7046..48d961d1 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1917,14 +1917,16 @@ that these may be overwritten)."
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.
 No effect if prover is busy."
-  (and (> (proof-queue-or-locked-end) beg)
-       (not (and (proof-inside-comment beg)
-		 (proof-inside-comment end)))
-       (if proof-shell-busy
-	   (error "Prover busy")
-	 (save-excursion
-	   (goto-char beg)
-	   (proof-retract-until-point)))))
+  (when (and (> (proof-queue-or-locked-end) beg)
+	     (not (and (proof-inside-comment beg)
+		       (proof-inside-comment end))))
+    (when proof-shell-busy
+      (message "Interrupting prover")
+      (proof-interrupt-process)
+      (proof-shell-wait))
+    (save-excursion
+      (goto-char beg)
+      (proof-retract-until-point))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3