clarified bootstrap process: switch to ML with context and antiquotations earlier;
authorwenzelm
Tue Mar 18 13:36:28 2014 +0100 (2014-03-18)
changeset 5620376c72f4d0667
parent 56202 0a11d17eeeff
child 56204 f70e69208a8c
clarified bootstrap process: switch to ML with context and antiquotations earlier;
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ROOT.ML
src/Pure/Thy/term_style.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Mar 18 12:25:17 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Mar 18 13:36:28 2014 +0100
     1.3 @@ -288,7 +288,7 @@
     1.4  fun isar in_stream term : isar =
     1.5    Source.tty in_stream
     1.6    |> Symbol.source
     1.7 -  |> Source.map_filter (fn "\\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
     1.8 +  |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
     1.9    |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
    1.10    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    1.11  
     2.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 18 12:25:17 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 13:36:28 2014 +0100
     2.3 @@ -22,6 +22,7 @@
     2.4    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     2.5      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
     2.6    val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
     2.7 +  val eval_file: bool -> Path.T -> unit
     2.8    val eval_source: bool -> Symbol_Pos.source -> unit
     2.9    val eval_in: Proof.context option -> bool -> Position.T ->
    2.10      ML_Lex.token Antiquote.antiquote list -> unit
    2.11 @@ -174,6 +175,10 @@
    2.12  
    2.13  (* derived versions *)
    2.14  
    2.15 +fun eval_file verbose path =
    2.16 +  let val pos = Path.position path
    2.17 +  in eval verbose pos (ML_Lex.read pos (File.read path)) end;
    2.18 +
    2.19  fun eval_source verbose source =
    2.20    eval verbose (#pos source) (ML_Lex.read_source source);
    2.21  
     3.1 --- a/src/Pure/ML/ml_env.ML	Tue Mar 18 12:25:17 2014 +0100
     3.2 +++ b/src/Pure/ML/ml_env.ML	Tue Mar 18 13:36:28 2014 +0100
     3.3 @@ -20,23 +20,26 @@
     3.4  structure Env = Generic_Data
     3.5  (
     3.6    type T =
     3.7 -    ML_Name_Space.valueVal Symtab.table *
     3.8 -    ML_Name_Space.typeVal Symtab.table *
     3.9 -    ML_Name_Space.fixityVal Symtab.table *
    3.10 -    ML_Name_Space.structureVal Symtab.table *
    3.11 -    ML_Name_Space.signatureVal Symtab.table *
    3.12 -    ML_Name_Space.functorVal Symtab.table;
    3.13 -  val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
    3.14 -  val extend = I;
    3.15 +    bool * (*global bootstrap environment*)
    3.16 +     (ML_Name_Space.valueVal Symtab.table *
    3.17 +      ML_Name_Space.typeVal Symtab.table *
    3.18 +      ML_Name_Space.fixityVal Symtab.table *
    3.19 +      ML_Name_Space.structureVal Symtab.table *
    3.20 +      ML_Name_Space.signatureVal Symtab.table *
    3.21 +      ML_Name_Space.functorVal Symtab.table);
    3.22 +  val empty : T =
    3.23 +    (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
    3.24 +  fun extend (_, tabs) : T = (false, tabs);
    3.25    fun merge
    3.26 -   ((val1, type1, fixity1, structure1, signature1, functor1),
    3.27 -    (val2, type2, fixity2, structure2, signature2, functor2)) : T =
    3.28 -    (Symtab.merge (K true) (val1, val2),
    3.29 -     Symtab.merge (K true) (type1, type2),
    3.30 -     Symtab.merge (K true) (fixity1, fixity2),
    3.31 -     Symtab.merge (K true) (structure1, structure2),
    3.32 -     Symtab.merge (K true) (signature1, signature2),
    3.33 -     Symtab.merge (K true) (functor1, functor2));
    3.34 +   ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
    3.35 +    (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
    3.36 +    (false,
    3.37 +     (Symtab.merge (K true) (val1, val2),
    3.38 +      Symtab.merge (K true) (type1, type2),
    3.39 +      Symtab.merge (K true) (fixity1, fixity2),
    3.40 +      Symtab.merge (K true) (structure1, structure2),
    3.41 +      Symtab.merge (K true) (signature1, signature2),
    3.42 +      Symtab.merge (K true) (functor1, functor2)));
    3.43  );
    3.44  
    3.45  val inherit = Env.put o Env.get;
    3.46 @@ -48,18 +51,22 @@
    3.47    let
    3.48      fun lookup sel1 sel2 name =
    3.49        Context.thread_data ()
    3.50 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
    3.51 +      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
    3.52        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    3.53  
    3.54      fun all sel1 sel2 () =
    3.55        Context.thread_data ()
    3.56 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
    3.57 +      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
    3.58        |> append (sel2 ML_Name_Space.global ())
    3.59        |> sort_distinct (string_ord o pairself #1);
    3.60  
    3.61      fun enter ap1 sel2 entry =
    3.62        if is_some (Context.thread_data ()) then
    3.63 -        Context.>> (Env.map (ap1 (Symtab.update entry)))
    3.64 +        Context.>> (Env.map (fn (global, tabs) =>
    3.65 +          let
    3.66 +            val _ = if global then sel2 ML_Name_Space.global entry else ();
    3.67 +            val tabs' = ap1 (Symtab.update entry) tabs;
    3.68 +          in (global, tabs') end))
    3.69        else sel2 ML_Name_Space.global entry;
    3.70    in
    3.71     {lookupVal    = lookup #1 #lookupVal,
     4.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 12:25:17 2014 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 13:36:28 2014 +0100
     4.3 @@ -39,7 +39,7 @@
     4.4  use "ML/ml_lex.ML";
     4.5  use "ML/ml_parse.ML";
     4.6  use "General/secure.ML";
     4.7 -(*^^^^^ end of basic ML bootstrap ^^^^^*)
     4.8 +(*^^^^^ end of ML bootstrap 0 ^^^^^*)
     4.9  use "General/integer.ML";
    4.10  use "General/stack.ML";
    4.11  use "General/queue.ML";
    4.12 @@ -222,7 +222,6 @@
    4.13  use "Isar/keyword.ML";
    4.14  use "Isar/parse.ML";
    4.15  use "Isar/args.ML";
    4.16 -use "ML/ml_context.ML";
    4.17  
    4.18  (*theory sources*)
    4.19  use "Thy/thy_header.ML";
    4.20 @@ -230,6 +229,11 @@
    4.21  use "Thy/html.ML";
    4.22  use "Thy/latex.ML";
    4.23  
    4.24 +(*ML with context and antiquotations*)
    4.25 +use "ML/ml_context.ML";
    4.26 +val use = ML_Context.eval_file true o Path.explode;
    4.27 +(*^^^^^ end of ML bootstrap 1 ^^^^^*)
    4.28 +
    4.29  (*basic proof engine*)
    4.30  use "Isar/proof_display.ML";
    4.31  use "Isar/attrib.ML";
     5.1 --- a/src/Pure/Thy/term_style.ML	Tue Mar 18 12:25:17 2014 +0100
     5.2 +++ b/src/Pure/Thy/term_style.ML	Tue Mar 18 13:36:28 2014 +0100
     5.3 @@ -68,8 +68,8 @@
     5.4    end);
     5.5  
     5.6  fun sub_symbols (d :: s :: ss) =
     5.7 -      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
     5.8 -      then d :: "\\<^sub>" :: sub_symbols (s :: ss)
     5.9 +      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s)
    5.10 +      then d :: "\<^sub>" :: sub_symbols (s :: ss)
    5.11        else d :: s :: ss
    5.12    | sub_symbols cs = cs;
    5.13