From d226fe5c9645fdd37dbd087db17a1673599c2a07 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 19 Oct 1999 15:30:23 +0000
Subject: Deactivate scripting before retracting a theory file. Fix for DvO's
 report.

---
 isa/isa.el | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/isa/isa.el b/isa/isa.el
index 9b2bd7ab..556dbb86 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -366,8 +366,13 @@ Resulting output from Isabelle will be parsed by Proof General."
   :group 'isabelle-config)
 
 (defun isa-retract-thy-file (file)
-  "Retract the theory file FILE. If interactive, use buffer-file-name."
+  "Retract the theory file FILE. If interactive, use buffer-file-name.
+To prevent inconsistencies, scripting is deactivated before doing this. 
+So if scripting is active in an ML file which is not completely processed, 
+you will be asked to retract the file or process the remainder of it.  
+(If you process the rest of it it may subsequently be unlocked anyway). "
   (interactive (list buffer-file-name))
+  (proof-deactivate-scripting)
   (proof-shell-invisible-command
    (format isa-retract-thy-file-command
 	   (file-name-nondirectory (file-name-sans-extension file)))))
-- 
cgit v1.2.3