clarified bootstrap process: switch to ML with context and antiquotations earlier;

--- a/src/Pure/Isar/outer_syntax.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -288,7 +288,7 @@
 fun isar in_stream term : isar =
   Source.tty in_stream
   |> Symbol.source
-  |> Source.map_filter (fn "\\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
+  |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) lookup_commands_dynamic;
 

--- a/src/Pure/ML/ml_context.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -22,6 +22,7 @@
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
+  val eval_file: bool -> Path.T -> unit
   val eval_source: bool -> Symbol_Pos.source -> unit
   val eval_in: Proof.context option -> bool -> Position.T ->
     ML_Lex.token Antiquote.antiquote list -> unit
@@ -174,6 +175,10 @@
 
 (* derived versions *)
 
+fun eval_file verbose path =
+  let val pos = Path.position path
+  in eval verbose pos (ML_Lex.read pos (File.read path)) end;
+
 fun eval_source verbose source =
   eval verbose (#pos source) (ML_Lex.read_source source);
 

--- a/src/Pure/ML/ml_env.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/ML/ml_env.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -20,23 +20,26 @@
 structure Env = Generic_Data
 (
   type T =
-    ML_Name_Space.valueVal Symtab.table *
-    ML_Name_Space.typeVal Symtab.table *
-    ML_Name_Space.fixityVal Symtab.table *
-    ML_Name_Space.structureVal Symtab.table *
-    ML_Name_Space.signatureVal Symtab.table *
-    ML_Name_Space.functorVal Symtab.table;
-  val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
-  val extend = I;
+    bool * (*global bootstrap environment*)
+     (ML_Name_Space.valueVal Symtab.table *
+      ML_Name_Space.typeVal Symtab.table *
+      ML_Name_Space.fixityVal Symtab.table *
+      ML_Name_Space.structureVal Symtab.table *
+      ML_Name_Space.signatureVal Symtab.table *
+      ML_Name_Space.functorVal Symtab.table);
+  val empty : T =
+    (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
+  fun extend (_, tabs) : T = (false, tabs);
   fun merge
-   ((val1, type1, fixity1, structure1, signature1, functor1),
-    (val2, type2, fixity2, structure2, signature2, functor2)) : T =
-    (Symtab.merge (K true) (val1, val2),
-     Symtab.merge (K true) (type1, type2),
-     Symtab.merge (K true) (fixity1, fixity2),
-     Symtab.merge (K true) (structure1, structure2),
-     Symtab.merge (K true) (signature1, signature2),
-     Symtab.merge (K true) (functor1, functor2));
+   ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
+    (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
+    (false,
+     (Symtab.merge (K true) (val1, val2),
+      Symtab.merge (K true) (type1, type2),
+      Symtab.merge (K true) (fixity1, fixity2),
+      Symtab.merge (K true) (structure1, structure2),
+      Symtab.merge (K true) (signature1, signature2),
+      Symtab.merge (K true) (functor1, functor2)));
 );
 
 val inherit = Env.put o Env.get;
@@ -48,18 +51,22 @@
   let
     fun lookup sel1 sel2 name =
       Context.thread_data ()
-      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
+      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
       |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
     fun all sel1 sel2 () =
       Context.thread_data ()
-      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
+      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
       |> append (sel2 ML_Name_Space.global ())
       |> sort_distinct (string_ord o pairself #1);
 
     fun enter ap1 sel2 entry =
       if is_some (Context.thread_data ()) then
-        Context.>> (Env.map (ap1 (Symtab.update entry)))
+        Context.>> (Env.map (fn (global, tabs) =>
+          let
+            val _ = if global then sel2 ML_Name_Space.global entry else ();
+            val tabs' = ap1 (Symtab.update entry) tabs;
+          in (global, tabs') end))
       else sel2 ML_Name_Space.global entry;
   in
    {lookupVal    = lookup #1 #lookupVal,

--- a/src/Pure/ROOT.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -39,7 +39,7 @@
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
-(*^^^^^ end of basic ML bootstrap ^^^^^*)
+(*^^^^^ end of ML bootstrap 0 ^^^^^*)
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
@@ -222,7 +222,6 @@
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
-use "ML/ml_context.ML";
 
 (*theory sources*)
 use "Thy/thy_header.ML";
@@ -230,6 +229,11 @@
 use "Thy/html.ML";
 use "Thy/latex.ML";
 
+(*ML with context and antiquotations*)
+use "ML/ml_context.ML";
+val use = ML_Context.eval_file true o Path.explode;
+(*^^^^^ end of ML bootstrap 1 ^^^^^*)
+
 (*basic proof engine*)
 use "Isar/proof_display.ML";
 use "Isar/attrib.ML";

--- a/src/Pure/Thy/term_style.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/Thy/term_style.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -68,8 +68,8 @@
   end);
 
 fun sub_symbols (d :: s :: ss) =
-      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
-      then d :: "\\<^sub>" :: sub_symbols (s :: ss)
+      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s)
+      then d :: "\<^sub>" :: sub_symbols (s :: ss)
       else d :: s :: ss
   | sub_symbols cs = cs;