1.1 --- a/src/Pure/General/secure.ML	Mon Dec 11 19:05:20 2006 +0100
     1.2 +++ b/src/Pure/General/secure.ML	Mon Dec 11 19:05:23 2006 +0100
     1.3 @@ -10,8 +10,9 @@
     1.4    val set_secure: unit -> unit
     1.5    val is_secure: unit -> bool
     1.6    val deny_secure: string -> unit
     1.7 +  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
     1.8 +  val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
     1.9    val use: string -> unit
    1.10 -  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    1.11    val commit: unit -> unit
    1.12    val execute: string -> string
    1.13    val system: string -> int
    1.14 @@ -36,11 +37,12 @@
    1.15  
    1.16  fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
    1.17  
    1.18 -val orig_use = use;
    1.19  val orig_use_text = use_text;
    1.20 +val orig_use_file = use_file;
    1.21  
    1.22 -fun use file = (secure_mltext (); orig_use file);
    1.23  fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt);
    1.24 +fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
    1.25 +val use = use_file Output.ml_output true;
    1.26  
    1.27  (*commit is dynamically bound!*)
    1.28  fun commit () = orig_use_text Output.ml_output false "commit();";
    1.29 @@ -58,7 +60,8 @@
    1.30  
    1.31  end;
    1.32  
    1.33 +val use_text = Secure.use_text;
    1.34 +val use_file = Secure.use_file;
    1.35  val use = Secure.use;
    1.36 -val use_text = Secure.use_text;
    1.37  val execute = Secure.execute;
    1.38  val system = Secure.system;

     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Mon Dec 11 19:05:20 2006 +0100
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Dec 11 19:05:23 2006 +0100
     2.3 @@ -144,6 +144,8 @@
     2.4      FileSys.remove tmp_name
     2.5    end;
     2.6  
     2.7 +fun use_file _ _ name = PolyML.use name;
     2.8 +
     2.9  
    2.10  
    2.11  (** interrupts **)      (*Note: may get into race conditions*)

     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Dec 11 19:05:20 2006 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Dec 11 19:05:23 2006 +0100
     3.3 @@ -111,6 +111,8 @@
     3.4      if verbose then print (output ()) else ()
     3.5    end;
     3.6  
     3.7 +fun use_file _ _ name = use name;
     3.8 +
     3.9  
    3.10  (*eval command line arguments*)
    3.11  local

     4.1 --- a/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:20 2006 +0100
     4.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:23 2006 +0100
     4.3 @@ -378,3 +378,4 @@
     4.4  end;
     4.5  
     4.6  fun use_text _ _ txt = use_string txt;
     4.7 +fun use_file _ _ name = use name;

     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Dec 11 19:05:20 2006 +0100
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 11 19:05:23 2006 +0100
     5.3 @@ -113,6 +113,9 @@
     5.4      if verbose then print (output ()) else ()
     5.5    end;
     5.6  
     5.7 +fun use_file _ _ name = use name;
     5.8 +
     5.9 +
    5.10  
    5.11  (** interrupts **)
    5.12