src/Pure/RAW/secure.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/secure.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -0,0 +1,27 @@
+(*  Title:      Pure/RAW/secure.ML
+    Author:     Makarius
+
+Secure critical operations.
+*)
+
+signature SECURE =
+sig
+  val set_secure: unit -> unit
+  val is_secure: unit -> bool
+  val deny: string -> unit
+  val deny_ml: unit -> unit
+end;
+
+structure Secure: SECURE =
+struct
+
+val secure = Unsynchronized.ref false;
+
+fun set_secure () = secure := true;
+fun is_secure () = ! secure;
+
+fun deny msg = if is_secure () then error msg else ();
+
+fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
+
+end;