From 3f56c3722de68e996e207d3cbf3f219aee96b5f3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 2 Oct 2009 17:31:24 +0000 Subject: proof-retract-before-change: give error if prover busy (see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293) --- generic/proof-script.el | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'generic/proof-script.el') 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." -- cgit v1.2.3