--- 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;