From a5255e9d42efa6586f91ae638cad3956efc0e93c Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Tue, 14 Aug 2012 09:50:13 +0000
Subject: fix 443 by enforcing that the prover is not busy in
 proof-retract-until-point

---
 generic/proof-script.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4ddb0045..d1c469a4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2219,8 +2219,11 @@ user hasn't saved the latest edits.  Therefore it is right to
 query saves here."
   (if (proof-locked-region-empty-p)
       (error "No locked region")
-    ;; enforces not busy (future: may allow retracting from queue in progress)
     (proof-activate-scripting)
+    ;; enforce not busy to avoid retracting items from the queue region,
+    ;; which is not supported currently, see #443
+    ;; (future: may allow retracting from queue in progress)
+    (proof-shell-ready-prover)
     (unless (proof-locked-region-empty-p) ;; re-opening may discard locked region!
       (let ((span (span-at (point) 'type)))
 	;; If no span at point, retracts the last span in the buffer.
-- 
cgit v1.2.3