# HG changeset patch
# User aspinall
# Date 1164277473 -3600
# Node ID fea600a852f8334b7055fa82ddd9a2395dae0d7e
# Parent  e4be91feca5086de21efe43b87b10cfaf12d7739
PGIP: add retractfile.  Be stricter in file open/close protocol.

diff -r e4be91feca50 -r fea600a852f8 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Nov 23 00:52:23 2006 +0100
+++ b/src/Pure/proof_general.ML	Thu Nov 23 11:24:33 2006 +0100
@@ -1295,18 +1295,28 @@
                            end
      (* improperfilecmd: theory-level commands not in script *)
      | "doitem"         => isarscript data
-     | "undoitem"       => isarcmd "ProofGeneral.undo"
+     | "undoitem"       => isarcmd "ProofGeneral.undo"  (* NB: named target not supported *)
      | "redoitem"       => isarcmd "ProofGeneral.redo"
      | "aborttheory"    => isarcmd ("init_toplevel")
      | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
-     | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
-     | "openfile"       => (openfile_retract (fileurl_of attrs);
-                            currently_open_file := SOME (fileurl_of attrs))
+     | "loadfile"       => (case !currently_open_file of
+                                SOME f => raise PGIP ("loadfile when a file is open!")
+                              | NONE => use_thy_or_ml_file (fileurl_of attrs))
+     | "openfile"       => (case !currently_open_file of
+                                SOME f => raise PGIP ("openfile when a file is already open!")
+                              | NONE => (openfile_retract (fileurl_of attrs);
+					 currently_open_file := SOME (fileurl_of attrs)))
      | "closefile"      => (case !currently_open_file of
                                 SOME f => (inform_file_processed f;
                                            currently_open_file := NONE)
                               | NONE => raise PGIP ("closefile when no file is open!"))
-     | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
+     | "abortfile"      => (case !currently_open_file of
+                                SOME f => (isarcmd "init_toplevel";
+					   currently_open_file := NONE)
+                              | NONE => raise PGIP ("abortfile when no file is open!"))
+     | "retractfile"    => (case !currently_open_file of
+                                SOME f => raise PGIP ("retractfile when a file is open!")
+                              | NONE => inform_file_retracted (fileurl_of attrs))
      | "changecwd"      => changecwd (dirname_attr attrs)
      | "systemcmd"      => isarscript data
      (* unofficial command for debugging *)