# HG changeset patch
# User wenzelm
# Date 1458320299 -3600
# Node ID 360d3464919ca8eefb70102223123c2797c00056
# Parent  254582abf06719c3bd290c6067c0031302255ca9
discontinued slightly odd "secure" mode;

diff -r 254582abf067 -r 360d3464919c src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Fri Mar 18 17:51:57 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      Pure/General/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;
diff -r 254582abf067 -r 360d3464919c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Fri Mar 18 17:58:19 2016 +0100
@@ -144,7 +144,6 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val _ = Secure.deny_ml ();
     val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
     val opt_context = Context.thread_data ();
 
diff -r 254582abf067 -r 360d3464919c src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:58:19 2016 +0100
@@ -47,8 +47,6 @@
 
 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
   let
-    val _ = Secure.deny_ml ();
-
     val current_line = Unsynchronized.ref line;
     val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
     val out_buffer = Unsynchronized.ref ([]: string list);
diff -r 254582abf067 -r 360d3464919c src/Pure/ROOT
--- a/src/Pure/ROOT	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/ROOT	Fri Mar 18 17:58:19 2016 +0100
@@ -47,7 +47,6 @@
     "General/random.ML"
     "General/same.ML"
     "General/scan.ML"
-    "General/secure.ML"
     "General/seq.ML"
     "General/sha1.ML"
     "General/socket_io.ML"
diff -r 254582abf067 -r 360d3464919c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/ROOT.ML	Fri Mar 18 17:58:19 2016 +0100
@@ -61,7 +61,6 @@
 
 (* ML compiler *)
 
-use "General/secure.ML";
 use "ML/ml_compiler0.ML";
 
 PolyML.Compiler.reportUnreferencedIds := true;
diff -r 254582abf067 -r 360d3464919c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 18 17:58:19 2016 +0100
@@ -14,15 +14,14 @@
     logic: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
-    secure: Boolean = false,
     receiver: Prover.Receiver = Console.println(_),
     store: Sessions.Store = Sessions.store()): Isabelle_Process =
   {
     val channel = System_Channel()
     val process =
       try {
-        ML_Process(options, logic = logic, args = args, modes = modes, secure = secure,
-          channel = Some(channel), store = store)
+        ML_Process(options, logic = logic, args = args, modes = modes, store = store,
+          channel = Some(channel))
       }
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
diff -r 254582abf067 -r 360d3464919c src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 17:51:57 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 17:58:19 2016 +0100
@@ -18,7 +18,6 @@
     dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     raw_ml_system: Boolean = false,
-    secure: Boolean = false,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
@@ -67,8 +66,6 @@
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
-    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
-
     val eval_process =
       if (heaps.isEmpty)
         List("PolyML.print_depth 10")
@@ -88,7 +85,7 @@
     // bash
     val bash_args =
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
-      (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+      (eval_init ::: eval_modes ::: eval_options ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),