diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1999-10-19 15:30:23 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-19 15:30:23 +0000 |
commit | d226fe5c9645fdd37dbd087db17a1673599c2a07 (patch) | |
tree | 985a929dab313778dc982229f1befad6511fb93a | |
parent | 42bfe6fd7de1867c5de38737aa1e637d39e5854c (diff) |
Deactivate scripting before retracting a theory file. Fix for DvO's report.
-rw-r--r-- | isa/isa.el | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -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))))) |