Secure critical operations.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/secure.ML	Mon Oct 09 19:37:04 2006 +0200
@@ -0,0 +1,47 @@
+(*  Title:      Pure/General/secure.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Secure critical operations.
+*)
+
+signature SECURE =
+sig
+  val set_secure: unit -> bool
+  val is_secure: unit -> bool
+  val deny_secure: string -> unit
+  val use: string -> unit
+  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
+  val commit: unit -> unit
+end;
+
+structure Secure: SECURE =
+struct
+
+(* secure flag *)
+
+val secure = ref false;
+
+fun set_secure () = set secure;
+fun is_secure () = ! secure;
+
+fun deny_secure msg = deny (is_secure ()) msg;
+
+
+(* critical operations *)
+
+fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
+
+val orig_use = use;
+val orig_use_text = use_text;
+
+fun use file = (secure_mltext (); orig_use file);
+fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt);
+
+(*commit is dynamically bound!*)
+fun commit () = orig_use_text Output.ml_output false "commit();";
+
+end;
+
+val use = Secure.use;
+val use_text = Secure.use_text;