From b34ddba34b88e08dde2e37b8eb357fd76300ed43 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 2 Nov 1998 17:22:29 +0000
Subject: Quick fix for multiple file problem when current scripting buffer is
 retracted by prover.

---
 generic/proof-script.el | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 624a468e..2b6de678 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -859,8 +859,9 @@ deletes the region corresponding to the proof sequence."
   (let ((start (span-start span))
         (end (span-end span))
 	(kill (span-property span 'delete-me)))
-    (proof-set-locked-end start)
-    (proof-set-queue-end start)
+    (unless (proof-locked-region-empty-p)
+      (proof-set-locked-end start)
+      (proof-set-queue-end start))
     (delete-spans start end 'type)
     (delete-span span)
     (if kill (delete-region start end))))
-- 
cgit v1.2.3