# HG changeset patch
# User wenzelm
# Date 1185375945 -7200
# Node ID 6e8d5a05ffe844d79b8aa70e13c597a87ad11b1a
# Parent  5a3ec03c825bd218ef6315593b56af6bcc1ff0b7
added use_noncritical;

diff -r 5a3ec03c825b -r 6e8d5a05ffe8 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Wed Jul 25 10:19:01 2007 +0200
+++ b/src/Pure/General/secure.ML	Wed Jul 25 17:05:45 2007 +0200
@@ -11,6 +11,7 @@
   val is_secure: unit -> bool
   val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
+  val use_noncritical: string -> unit
   val use: string -> unit
   val commit: unit -> unit
   val execute: string -> string
@@ -45,7 +46,10 @@
 fun use_file pr verbose name = CRITICAL (fn () =>
   (secure_mltext (); orig_use_file pr verbose name));
 
-fun use name = CRITICAL (fn () => use_file Output.ml_output true name);
+fun use name = use_file Output.ml_output true name;
+
+fun use_noncritical name =
+  (secure_mltext (); orig_use_file Output.ml_output true name);
 
 (*commit is dynamically bound!*)
 fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
@@ -63,6 +67,7 @@
 
 end;
 
+(*override previous toplevel bindings!*)
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 val use = Secure.use;