# HG changeset patch
# User wenzelm
# Date 1165860323 -3600
# Node ID ea6f846d8c4ba63981bf8625950e3ddadf34de57
# Parent  b82f344f7922871ea4cc8dc96d50a89bcbf8d383
added use_file;

diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/General/secure.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -10,8 +10,9 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
+  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
+  val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
-  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val commit: unit -> unit
   val execute: string -> string
   val system: string -> int
@@ -36,11 +37,12 @@
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
-val orig_use = use;
 val orig_use_text = use_text;
+val orig_use_file = use_file;
 
-fun use file = (secure_mltext (); orig_use file);
 fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt);
+fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
+val use = use_file Output.ml_output true;
 
 (*commit is dynamically bound!*)
 fun commit () = orig_use_text Output.ml_output false "commit();";
@@ -58,7 +60,8 @@
 
 end;
 
+val use_text = Secure.use_text;
+val use_file = Secure.use_file;
 val use = Secure.use;
-val use_text = Secure.use_text;
 val execute = Secure.execute;
 val system = Secure.system;
diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -144,6 +144,8 @@
     FileSys.remove tmp_name
   end;
 
+fun use_file _ _ name = PolyML.use name;
+
 
 
 (** interrupts **)      (*Note: may get into race conditions*)
diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -111,6 +111,8 @@
     if verbose then print (output ()) else ()
   end;
 
+fun use_file _ _ name = use name;
+
 
 (*eval command line arguments*)
 local
diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -378,3 +378,4 @@
 end;
 
 fun use_text _ _ txt = use_string txt;
+fun use_file _ _ name = use name;
diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -113,6 +113,9 @@
     if verbose then print (output ()) else ()
   end;
 
+fun use_file _ _ name = use name;
+
+
 
 (** interrupts **)