proof-retract-before-change: give error if prover busy

(see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293)

1 files changed, 7 insertions, 4 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 6435c373..40249215 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2087,13 +2087,16 @@ that these may be overwritten)."
     (proof-extend-queue lastpos vanillas)))
 
 (defun proof-retract-before-change (beg end)
-  "For `before-change-functions'.  Retract to BEG unless BEG..END in comment."
+  "For `before-change-functions'.  Retract to BEG unless BEG..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)))
-       (save-excursion
-	 (goto-char beg)
-	 (proof-retract-until-point))))
+       (if proof-shell-busy
+	   (error "Prover busy")
+	 (save-excursion
+	   (goto-char beg)
+	   (proof-retract-until-point)))))
 
 (defun proof-inside-comment (pos)
   "Returns non-nil if POS is inside a comment."