support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;

--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -197,8 +197,8 @@
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
     val flags: ML_Compiler.flags =
-      {SML = false, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = false, SML_env = false, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -211,8 +211,8 @@
     val ([{lines, pos, ...}: Token.file], thy') = files thy;
     val source = Input.source true (cat_lines lines) (pos, pos);
     val flags: ML_Compiler.flags =
-      {SML = true, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = true, SML_env = true, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     thy' |> Context.theory_map
       (ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -255,8 +255,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -267,8 +267,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>

--- a/src/Pure/ML/ML_Root.thy	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/ML/ML_Root.thy	Tue Apr 05 18:20:25 2016 +0200
@@ -10,6 +10,8 @@
   and "use_thy" :: thy_load
 begin
 
+setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
+
 ML \<open>
 local
 

--- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+    {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
@@ -21,18 +21,19 @@
 (* flags *)
 
 type flags =
-  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+  {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {SML = false, exchange = false, redirect = false, verbose = false,
+  {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
-    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+  {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
+    redirect = #redirect flags, verbose = b, debug = #debug flags,
+    writeln = #writeln flags, warning = #warning flags};
 
 
 (* parse trees *)
@@ -144,7 +145,7 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
+    val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
     val opt_context = Context.thread_data ();
 
 
@@ -153,7 +154,7 @@
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_explode =
-      if #SML flags then String.explode
+      if #SML_syntax flags then String.explode
       else maps (String.explode o Symbol.esc) o Symbol.explode;
 
     val input_buffer =

--- a/src/Pure/ML/ml_context.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -218,7 +218,7 @@
   in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
-  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
+  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_thread_data (Option.map Context.Proof ctxt)

--- a/src/Pure/ML/ml_env.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -12,6 +12,7 @@
   val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
     Context.generic -> Context.generic
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
+  val init_bootstrap: Context.generic -> Context.generic
   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
   val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val context: ML_Compiler0.context
@@ -92,6 +93,23 @@
 
 (* name space *)
 
+val init_bootstrap =
+  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
+    let
+      val sml_tables' =
+        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
+            let
+              val val2 =
+                fold (fn (x, y) =>
+                  member (op =) ML_Name_Space.excluded_values x ? Symtab.update (x, y))
+                (#allVal ML_Name_Space.global ()) val1;
+              val structure2 =
+                fold (fn (x, y) =>
+                  member (op =) ML_Name_Space.excluded_structures x ? Symtab.update (x, y))
+                (#allStruct ML_Name_Space.global ()) structure1;
+            in (val2, type1, fixity1, structure2, signature1, functor1) end);
+    in make_data (bootstrap, tables, sml_tables', breakpoints) end);
+
 fun add_name_space {SML} (space: ML_Name_Space.T) =
   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     let

--- a/src/Pure/ML/ml_file.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/ML/ml_file.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -19,9 +19,10 @@
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
+    val (SML_syntax, SML_env) = SML src_path;
     val flags =
-      {SML = SML src_path, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -29,15 +30,15 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command (K false);
-val SML = command (K true);
+val ML = command (K (false, false));
+val SML = command (K (true, true));
 
 val use =
   command (fn path =>
     (case try (#2 o Path.split_ext) path of
-      SOME "ML" => false
-    | SOME "sml" => true
-    | SOME "sig" => true
+      SOME "ML" => (false, true)
+    | SOME "sml" => (true, true)
+    | SOME "sig" => (true, true)
     | _ =>
         error ("Bad file name " ^ Path.print path ^
           "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));

--- a/src/Pure/Pure.thy	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 05 18:20:25 2016 +0200
@@ -133,8 +133,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -145,8 +145,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>

--- a/src/Pure/Tools/debugger.ML	Tue Apr 05 18:18:36 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 18:20:25 2016 +0200
@@ -143,7 +143,7 @@
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {SML = SML, exchange = false, redirect = false, verbose = verbose,
+    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;