# 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 **)