tuned;
authorwenzelm
Sun Aug 26 17:48:35 2018 +0200 (14 months ago)
changeset 688146a0b1357bded
parent 68813 78edc4bc3bd3
child 68815 6296915dee6e
tuned;
src/Pure/ML/ml_env.ML
     1.1 --- a/src/Pure/ML/ml_env.ML	Sun Aug 26 17:28:38 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Sun Aug 26 17:48:35 2018 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  structure ML_Env: ML_ENV =
     1.5  struct
     1.6  
     1.7 -(* context data *)
     1.8 +(* name space tables *)
     1.9  
    1.10  type tables =
    1.11    PolyML.NameSpace.Values.value Symtab.table *
    1.12 @@ -35,6 +35,9 @@
    1.13    PolyML.NameSpace.Signatures.signatureVal Symtab.table *
    1.14    PolyML.NameSpace.Functors.functorVal Symtab.table;
    1.15  
    1.16 +val empty_tables: tables =
    1.17 +  (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
    1.18 +
    1.19  fun merge_tables
    1.20    ((val1, type1, fixity1, structure1, signature1, functor1),
    1.21     (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    1.22 @@ -45,6 +48,33 @@
    1.23     Symtab.merge (K true) (signature1, signature2),
    1.24     Symtab.merge (K true) (functor1, functor2));
    1.25  
    1.26 +val sml_tables: tables =
    1.27 +  (Symtab.make ML_Name_Space.sml_val,
    1.28 +   Symtab.make ML_Name_Space.sml_type,
    1.29 +   Symtab.make ML_Name_Space.sml_fixity,
    1.30 +   Symtab.make ML_Name_Space.sml_structure,
    1.31 +   Symtab.make ML_Name_Space.sml_signature,
    1.32 +   Symtab.make ML_Name_Space.sml_functor);
    1.33 +
    1.34 +fun bootstrap_tables ((val1, type1, fixity1, structure1, signature1, functor1): tables) : tables =
    1.35 +  let
    1.36 +    val val2 =
    1.37 +      fold (fn (x, y) =>
    1.38 +        member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
    1.39 +      (#allVal ML_Name_Space.global ()) val1;
    1.40 +    val structure2 =
    1.41 +      fold (fn (x, y) =>
    1.42 +        member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
    1.43 +      (#allStruct ML_Name_Space.global ()) structure1;
    1.44 +    val signature2 =
    1.45 +      fold (fn (x, y) =>
    1.46 +        member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
    1.47 +      (#allSig ML_Name_Space.global ()) signature1;
    1.48 +  in (val2, type1, fixity1, structure2, signature2, functor1) end;
    1.49 +
    1.50 +
    1.51 +(* context data *)
    1.52 +
    1.53  type data =
    1.54   {global: bool,
    1.55    tables: tables,
    1.56 @@ -57,16 +87,7 @@
    1.57  structure Env = Generic_Data
    1.58  (
    1.59    type T = data
    1.60 -  val empty =
    1.61 -    make_data (true,
    1.62 -      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
    1.63 -      (Symtab.make ML_Name_Space.sml_val,
    1.64 -       Symtab.make ML_Name_Space.sml_type,
    1.65 -       Symtab.make ML_Name_Space.sml_fixity,
    1.66 -       Symtab.make ML_Name_Space.sml_structure,
    1.67 -       Symtab.make ML_Name_Space.sml_signature,
    1.68 -       Symtab.make ML_Name_Space.sml_functor),
    1.69 -      Inttab.empty);
    1.70 +  val empty = make_data (true, empty_tables, sml_tables, Inttab.empty);
    1.71    fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
    1.72    fun merge (data : T * T) =
    1.73      make_data (false,
    1.74 @@ -113,24 +134,7 @@
    1.75  
    1.76  val init_bootstrap =
    1.77    Env.map (fn {global, tables, sml_tables, breakpoints} =>
    1.78 -    let
    1.79 -      val sml_tables' =
    1.80 -        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
    1.81 -            let
    1.82 -              val val2 =
    1.83 -                fold (fn (x, y) =>
    1.84 -                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
    1.85 -                (#allVal ML_Name_Space.global ()) val1;
    1.86 -              val structure2 =
    1.87 -                fold (fn (x, y) =>
    1.88 -                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
    1.89 -                (#allStruct ML_Name_Space.global ()) structure1;
    1.90 -              val signature2 =
    1.91 -                fold (fn (x, y) =>
    1.92 -                  member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
    1.93 -                (#allSig ML_Name_Space.global ()) signature1;
    1.94 -            in (val2, type1, fixity1, structure2, signature2, functor1) end);
    1.95 -    in make_data (global, tables, sml_tables', breakpoints) end);
    1.96 +    make_data (global, tables, bootstrap_tables sml_tables, breakpoints));
    1.97  
    1.98  fun set_global global =
    1.99    Env.map (fn {tables, sml_tables, breakpoints, ...} =>