# HG changeset patch
# User wenzelm
# Date 1456863029 -3600
# Node ID dd154240a53cea4192b227e1d52ce7770a7c26df
# Parent  0e53fade87fe8dd2c20762f6b98c61b9c46cfe2b
load secure.ML earlier;
eliminated obsolete ml_parse.ML;
tuned signature;

diff -r 0e53fade87fe -r dd154240a53c src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -206,7 +206,7 @@
 
 fun exec verbose code =
   ML_Context.exec (fn () =>
-    Secure.use_text ML_Env.local_context
+    use_text ML_Env.local_context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
diff -r 0e53fade87fe -r dd154240a53c src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Mar 01 21:00:38 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +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_secure: string -> unit
-  val secure_mltext: unit -> unit
-  val use_text: use_context ->
-    {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
-  val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
-end;
-
-structure Secure: SECURE =
-struct
-
-(** secure flag **)
-
-val secure = Unsynchronized.ref false;
-
-fun set_secure () = secure := true;
-fun is_secure () = ! secure;
-
-fun deny_secure msg = if is_secure () then error msg else ();
-
-
-
-(** critical operations **)
-
-fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
-
-val raw_use_text = use_text;
-val raw_use_file = use_file;
-
-fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
-fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
-
-end;
diff -r 0e53fade87fe -r dd154240a53c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -148,7 +148,7 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val _ = Secure.secure_mltext ();
+    val _ = Secure.deny_ml ();
     val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
     val opt_context = Context.thread_data ();
 
diff -r 0e53fade87fe -r dd154240a53c src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -164,7 +164,7 @@
 
 val local_context: use_context =
  {name_space = name_space {SML = false, exchange = false},
-  str_of_pos = Position.here oo Position.line_file,
+  here = Position.here oo Position.line_file,
   print = writeln,
   error = error};
 
diff -r 0e53fade87fe -r dd154240a53c src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Tue Mar 01 21:00:38 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:      Pure/ML/ml_parse.ML
-    Author:     Makarius
-
-Minimal parsing for SML -- fixing integer numerals.
-*)
-
-signature ML_PARSE =
-sig
-  val global_context: use_context
-end;
-
-structure ML_Parse: ML_PARSE =
-struct
-
-(** error handling **)
-
-fun !!! scan =
-  let
-    fun get_pos [] = " (end-of-input)"
-      | get_pos (tok :: _) = Position.here (ML_Lex.pos_of tok);
-
-    fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
-      | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
-  in Scan.!! err scan end;
-
-fun bad_input x =
-  (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
-    (fn msg => Scan.fail_with (K (fn () => msg)))) x;
-
-
-(** basic parsers **)
-
-fun $$$ x =
-  Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Keyword andalso ML_Lex.content_of tok = x)
-    >> ML_Lex.content_of;
-
-val int = Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Int) >> ML_Lex.content_of;
-
-val regular = Scan.one ML_Lex.is_regular >> ML_Lex.content_of;
-val improper = Scan.one ML_Lex.is_improper >> ML_Lex.content_of;
-
-val blanks = Scan.repeat improper >> implode;
-
-
-(* global use_context *)
-
-val global_context: use_context =
- {name_space = ML_Name_Space.global,
-  str_of_pos = Position.here oo Position.line_file,
-  print = writeln,
-  error = error};
-
-end;
diff -r 0e53fade87fe -r dd154240a53c src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -154,6 +154,8 @@
 
 (* ML compiler *)
 
+use "RAW/secure.ML";
+
 structure ML_Name_Space =
 struct
   open ML_Name_Space;
diff -r 0e53fade87fe -r dd154240a53c src/Pure/RAW/compiler_polyml.ML
--- a/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -5,7 +5,7 @@
 
 type use_context =
  {name_space: ML_Name_Space.T,
-  str_of_pos: int -> string -> string,
+  here: int -> string -> string,
   print: string -> unit,
   error: string -> unit};
 
@@ -13,9 +13,9 @@
 
 val boot_context: use_context =
  {name_space = ML_Name_Space.global,
-  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+  here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
   print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-  error = fn s => raise Fail s};
+  error = fn s => error s};
 
 fun drop_newline s =
   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
@@ -23,9 +23,11 @@
 
 in
 
-fun use_text ({name_space, str_of_pos, print, error, ...}: use_context)
+fun use_text ({name_space, here, print, error, ...}: use_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_positions line file text));
     val out_buffer = Unsynchronized.ref ([]: string list);
@@ -41,7 +43,7 @@
      (put (if hard then "Error: " else "Warning: ");
       PolyML.prettyPrint (put, 76) msg1;
       (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
-      put ("At" ^ str_of_pos (FixedInt.toInt message_line) file ^ "\n"));
+      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,
@@ -71,18 +73,12 @@
 fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
   | use_debug_option (SOME debug) = debug;
 
-local
-
-fun use_ opt_debug file =
-  use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
-    handle Fail msg => (#print boot_context msg; raise Fail "ML error");
+fun use_operations (use_ : bool option -> string -> unit) =
+  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
 
-in
-
-val use = use_ NONE;
-val use_debug = use_ (SOME true);
-val use_no_debug = use_ (SOME false);
+val {use, use_debug, use_no_debug} =
+  use_operations (fn opt_debug => fn file =>
+    use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
+      handle ERROR msg => (#print boot_context msg; raise error "ML error"));
 
 end;
-
-end;
diff -r 0e53fade87fe -r dd154240a53c 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;
diff -r 0e53fade87fe -r dd154240a53c src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ROOT	Tue Mar 01 21:10:29 2016 +0100
@@ -28,6 +28,7 @@
     "RAW/ml_stack_polyml-5.6.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
+    "RAW/secure.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
@@ -59,6 +60,7 @@
     "RAW/ml_stack_polyml-5.6.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
+    "RAW/secure.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
@@ -105,7 +107,6 @@
     "General/queue.ML"
     "General/same.ML"
     "General/scan.ML"
-    "General/secure.ML"
     "General/seq.ML"
     "General/sha1.ML"
     "General/sha1_polyml.ML"
@@ -166,7 +167,6 @@
     "ML/ml_file.ML"
     "ML/ml_lex.ML"
     "ML/ml_options.ML"
-    "ML/ml_parse.ML"
     "ML/ml_statistics.ML"
     "ML/ml_statistics_dummy.ML"
     "ML/ml_syntax.ML"
diff -r 0e53fade87fe -r dd154240a53c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -1,6 +1,6 @@
 (*** Isabelle/Pure bootstrap from "RAW" environment ***)
 
-(** bootstrap phase 0: towards secure ML barrier *)
+(** bootstrap phase 0: towards ML within position context *)
 
 structure Distribution =     (*filled-in by makedist*)
 struct
@@ -33,24 +33,21 @@
 use "General/input.ML";
 use "General/antiquote.ML";
 use "ML/ml_lex.ML";
-use "ML/ml_parse.ML";
-use "General/secure.ML";
 
-val use_text = Secure.use_text;
-val use_file = Secure.use_file;
-
-local
-  fun use_ opt_debug file =
-    Position.setmp_thread_data (Position.file_only file)
-      (fn () =>
-        Secure.use_file ML_Parse.global_context
-          {verbose = true, debug = use_debug_option opt_debug} file
-        handle ERROR msg => (writeln msg; error "ML error")) ();
-in
-  val use = use_ NONE;
-  val use_debug = use_ (SOME true);
-  val use_no_debug = use_ (SOME false);
-end;
+val {use, use_debug, use_no_debug} =
+  let
+    val global_context: use_context =
+     {name_space = ML_Name_Space.global,
+      here = Position.here oo Position.line_file,
+      print = writeln,
+      error = error}
+  in
+    use_operations (fn opt_debug => fn file =>
+      Position.setmp_thread_data (Position.file_only file)
+        (fn () =>
+          use_file global_context {verbose = true, debug = use_debug_option opt_debug} file
+            handle ERROR msg => (writeln msg; error "ML error")) ())
+  end;
 
 
 
@@ -230,19 +227,12 @@
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
-local
-  fun use_ opt_debug file =
-    let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
+val {use, use_debug, use_no_debug} =
+  use_operations (fn opt_debug => fn file =>
+    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
       ML_Context.eval_file flags (Path.explode file)
         handle ERROR msg => (writeln msg; error "ML error")
-    end;
-in
-
-val use = use_ NONE;
-val use_debug = use_ (SOME true);
-val use_no_debug = use_ (SOME false);
-
-end;
+    end);
 
 
 
diff -r 0e53fade87fe -r dd154240a53c src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -82,7 +82,7 @@
 fun exec ctxt verbose code =
  (if Config.get ctxt trace then tracing code else ();
   ML_Context.exec (fn () =>
-    Secure.use_text ML_Env.local_context
+    use_text ML_Env.local_context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -529,7 +529,7 @@
     allStruct    = #allStruct ML_Env.local_name_space,
     allSig       = #allSig ML_Env.local_name_space,
     allFunct     = #allFunct ML_Env.local_name_space},
-  str_of_pos = #str_of_pos ML_Env.local_context,
+  here = #here ML_Env.local_context,
   print = #print ML_Env.local_context,
   error = #error ML_Env.local_context};
 
@@ -540,7 +540,7 @@
     val thy' = Loaded_Values.put [] thy;
     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
     val _ =
-      Secure.use_text notifying_context
+      use_text notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
         (File.read filepath);
     val thy'' = Context.the_theory (Context.the_thread_data ());
diff -r 0e53fade87fe -r dd154240a53c src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -129,13 +129,13 @@
     val return = Unsynchronized.ref "return"
     val use_context : use_context =
      {name_space = #name_space ML_Env.local_context,
-      str_of_pos = #str_of_pos ML_Env.local_context,
+      here = #here ML_Env.local_context,
       print = fn r => return := r,
       error = #error ML_Env.local_context}
     val _ =
       Context.setmp_thread_data (SOME (Context.Proof ctxt))
         (fn () =>
-          Secure.use_text use_context
+          use_text use_context
             {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   in
     Gen_Construction.parse_pred (! return)
@@ -145,7 +145,7 @@
 fun run_test ctxt s =
   Context.setmp_thread_data (SOME (Context.Proof ctxt))
     (fn () =>
-      Secure.use_text ML_Env.local_context
+      use_text ML_Env.local_context
         {line = 0, file = "generated code", verbose = false, debug = false} s) ();
 
 (*split input into tokens*)