discontinued slightly odd "secure" mode;
authorwenzelm
Fri Mar 18 17:58:19 2016 +0100 (2016-03-18)
changeset 62668360d3464919c
parent 62667 254582abf067
child 62669 c95b76681e65
discontinued slightly odd "secure" mode;
src/Pure/General/secure.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/General/secure.ML	Fri Mar 18 17:51:57 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,27 +0,0 @@
     1.4 -(*  Title:      Pure/General/secure.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Secure critical operations.
     1.8 -*)
     1.9 -
    1.10 -signature SECURE =
    1.11 -sig
    1.12 -  val set_secure: unit -> unit
    1.13 -  val is_secure: unit -> bool
    1.14 -  val deny: string -> unit
    1.15 -  val deny_ml: unit -> unit
    1.16 -end;
    1.17 -
    1.18 -structure Secure: SECURE =
    1.19 -struct
    1.20 -
    1.21 -val secure = Unsynchronized.ref false;
    1.22 -
    1.23 -fun set_secure () = secure := true;
    1.24 -fun is_secure () = ! secure;
    1.25 -
    1.26 -fun deny msg = if is_secure () then error msg else ();
    1.27 -
    1.28 -fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
    1.29 -
    1.30 -end;
     2.1 --- a/src/Pure/ML/ml_compiler.ML	Fri Mar 18 17:51:57 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_compiler.ML	Fri Mar 18 17:58:19 2016 +0100
     2.3 @@ -144,7 +144,6 @@
     2.4  
     2.5  fun eval (flags: flags) pos toks =
     2.6    let
     2.7 -    val _ = Secure.deny_ml ();
     2.8      val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
     2.9      val opt_context = Context.thread_data ();
    2.10  
     3.1 --- a/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:51:57 2016 +0100
     3.2 +++ b/src/Pure/ML/ml_compiler0.ML	Fri Mar 18 17:58:19 2016 +0100
     3.3 @@ -47,8 +47,6 @@
     3.4  
     3.5  fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
     3.6    let
     3.7 -    val _ = Secure.deny_ml ();
     3.8 -
     3.9      val current_line = Unsynchronized.ref line;
    3.10      val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
    3.11      val out_buffer = Unsynchronized.ref ([]: string list);
     4.1 --- a/src/Pure/ROOT	Fri Mar 18 17:51:57 2016 +0100
     4.2 +++ b/src/Pure/ROOT	Fri Mar 18 17:58:19 2016 +0100
     4.3 @@ -47,7 +47,6 @@
     4.4      "General/random.ML"
     4.5      "General/same.ML"
     4.6      "General/scan.ML"
     4.7 -    "General/secure.ML"
     4.8      "General/seq.ML"
     4.9      "General/sha1.ML"
    4.10      "General/socket_io.ML"
     5.1 --- a/src/Pure/ROOT.ML	Fri Mar 18 17:51:57 2016 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Fri Mar 18 17:58:19 2016 +0100
     5.3 @@ -61,7 +61,6 @@
     5.4  
     5.5  (* ML compiler *)
     5.6  
     5.7 -use "General/secure.ML";
     5.8  use "ML/ml_compiler0.ML";
     5.9  
    5.10  PolyML.Compiler.reportUnreferencedIds := true;
     6.1 --- a/src/Pure/System/isabelle_process.scala	Fri Mar 18 17:51:57 2016 +0100
     6.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Mar 18 17:58:19 2016 +0100
     6.3 @@ -14,15 +14,14 @@
     6.4      logic: String = "",
     6.5      args: List[String] = Nil,
     6.6      modes: List[String] = Nil,
     6.7 -    secure: Boolean = false,
     6.8      receiver: Prover.Receiver = Console.println(_),
     6.9      store: Sessions.Store = Sessions.store()): Isabelle_Process =
    6.10    {
    6.11      val channel = System_Channel()
    6.12      val process =
    6.13        try {
    6.14 -        ML_Process(options, logic = logic, args = args, modes = modes, secure = secure,
    6.15 -          channel = Some(channel), store = store)
    6.16 +        ML_Process(options, logic = logic, args = args, modes = modes, store = store,
    6.17 +          channel = Some(channel))
    6.18        }
    6.19        catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    6.20      process.stdin.close
     7.1 --- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 17:51:57 2016 +0100
     7.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 17:58:19 2016 +0100
     7.3 @@ -18,7 +18,6 @@
     7.4      dirs: List[Path] = Nil,
     7.5      modes: List[String] = Nil,
     7.6      raw_ml_system: Boolean = false,
     7.7 -    secure: Boolean = false,
     7.8      cwd: JFile = null,
     7.9      env: Map[String, String] = Isabelle_System.settings(),
    7.10      redirect: Boolean = false,
    7.11 @@ -67,8 +66,6 @@
    7.12      val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    7.13      val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
    7.14  
    7.15 -    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
    7.16 -
    7.17      val eval_process =
    7.18        if (heaps.isEmpty)
    7.19          List("PolyML.print_depth 10")
    7.20 @@ -88,7 +85,7 @@
    7.21      // bash
    7.22      val bash_args =
    7.23        Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    7.24 -      (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    7.25 +      (eval_init ::: eval_modes ::: eval_options ::: eval_process).
    7.26          map(eval => List("--eval", eval)).flatten ::: args
    7.27  
    7.28      Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),