# HG changeset patch
# User aspinall
# Date 1169640916 -3600
# Node ID 58f554f51f0d163284af0defdc279e23e601f470
# Parent  5682eeaefaf454aaf1701ca2ec8e0037d4937fe0
Let <loadfile> execute even while a file is open interactively.

diff -r 5682eeaefaf4 -r 58f554f51f0d src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 23 20:29:03 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 24 13:15:16 2007 +0100
@@ -849,10 +849,14 @@
     let
         val url = #url vs
     in
-        case !currently_open_file of
+        (* da: this doesn't seem to cause a problem, batch loading uses
+           a different state context.  Of course confusion is still possible,
+           e.g. file loaded depends on open file which is not yet saved. *)
+        (* case !currently_open_file of
             SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
 				  PgipTypes.string_of_pgipurl url)
-          | NONE => use_thy_or_ml_file (File.platform_path url)
+          | NONE => *)
+	use_thy_or_ml_file (File.platform_path url)
     end
 
 fun abortfile vs =