src/Pure/ML/ml_env.ML
changeset 68814 6a0b1357bded
parent 68813 78edc4bc3bd3
child 68816 5a53724fe247
equal deleted inserted replaced
68813:78edc4bc3bd3 68814:6a0b1357bded
    23 end
    23 end
    24 
    24 
    25 structure ML_Env: ML_ENV =
    25 structure ML_Env: ML_ENV =
    26 struct
    26 struct
    27 
    27 
    28 (* context data *)
    28 (* name space tables *)
    29 
    29 
    30 type tables =
    30 type tables =
    31   PolyML.NameSpace.Values.value Symtab.table *
    31   PolyML.NameSpace.Values.value Symtab.table *
    32   PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
    32   PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
    33   PolyML.NameSpace.Infixes.fixity Symtab.table *
    33   PolyML.NameSpace.Infixes.fixity Symtab.table *
    34   PolyML.NameSpace.Structures.structureVal Symtab.table *
    34   PolyML.NameSpace.Structures.structureVal Symtab.table *
    35   PolyML.NameSpace.Signatures.signatureVal Symtab.table *
    35   PolyML.NameSpace.Signatures.signatureVal Symtab.table *
    36   PolyML.NameSpace.Functors.functorVal Symtab.table;
    36   PolyML.NameSpace.Functors.functorVal Symtab.table;
       
    37 
       
    38 val empty_tables: tables =
       
    39   (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
    37 
    40 
    38 fun merge_tables
    41 fun merge_tables
    39   ((val1, type1, fixity1, structure1, signature1, functor1),
    42   ((val1, type1, fixity1, structure1, signature1, functor1),
    40    (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    43    (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    41   (Symtab.merge (K true) (val1, val2),
    44   (Symtab.merge (K true) (val1, val2),
    43    Symtab.merge (K true) (fixity1, fixity2),
    46    Symtab.merge (K true) (fixity1, fixity2),
    44    Symtab.merge (K true) (structure1, structure2),
    47    Symtab.merge (K true) (structure1, structure2),
    45    Symtab.merge (K true) (signature1, signature2),
    48    Symtab.merge (K true) (signature1, signature2),
    46    Symtab.merge (K true) (functor1, functor2));
    49    Symtab.merge (K true) (functor1, functor2));
    47 
    50 
       
    51 val sml_tables: tables =
       
    52   (Symtab.make ML_Name_Space.sml_val,
       
    53    Symtab.make ML_Name_Space.sml_type,
       
    54    Symtab.make ML_Name_Space.sml_fixity,
       
    55    Symtab.make ML_Name_Space.sml_structure,
       
    56    Symtab.make ML_Name_Space.sml_signature,
       
    57    Symtab.make ML_Name_Space.sml_functor);
       
    58 
       
    59 fun bootstrap_tables ((val1, type1, fixity1, structure1, signature1, functor1): tables) : tables =
       
    60   let
       
    61     val val2 =
       
    62       fold (fn (x, y) =>
       
    63         member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
       
    64       (#allVal ML_Name_Space.global ()) val1;
       
    65     val structure2 =
       
    66       fold (fn (x, y) =>
       
    67         member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
       
    68       (#allStruct ML_Name_Space.global ()) structure1;
       
    69     val signature2 =
       
    70       fold (fn (x, y) =>
       
    71         member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
       
    72       (#allSig ML_Name_Space.global ()) signature1;
       
    73   in (val2, type1, fixity1, structure2, signature2, functor1) end;
       
    74 
       
    75 
       
    76 (* context data *)
       
    77 
    48 type data =
    78 type data =
    49  {global: bool,
    79  {global: bool,
    50   tables: tables,
    80   tables: tables,
    51   sml_tables: tables,
    81   sml_tables: tables,
    52   breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
    82   breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
    55   {global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
    85   {global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
    56 
    86 
    57 structure Env = Generic_Data
    87 structure Env = Generic_Data
    58 (
    88 (
    59   type T = data
    89   type T = data
    60   val empty =
    90   val empty = make_data (true, empty_tables, sml_tables, Inttab.empty);
    61     make_data (true,
       
    62       (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
       
    63       (Symtab.make ML_Name_Space.sml_val,
       
    64        Symtab.make ML_Name_Space.sml_type,
       
    65        Symtab.make ML_Name_Space.sml_fixity,
       
    66        Symtab.make ML_Name_Space.sml_structure,
       
    67        Symtab.make ML_Name_Space.sml_signature,
       
    68        Symtab.make ML_Name_Space.sml_functor),
       
    69       Inttab.empty);
       
    70   fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
    91   fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
    71   fun merge (data : T * T) =
    92   fun merge (data : T * T) =
    72     make_data (false,
    93     make_data (false,
    73       merge_tables (apply2 #tables data),
    94       merge_tables (apply2 #tables data),
    74       merge_tables (apply2 #sml_tables data),
    95       merge_tables (apply2 #sml_tables data),
   111 
   132 
   112 (* name space *)
   133 (* name space *)
   113 
   134 
   114 val init_bootstrap =
   135 val init_bootstrap =
   115   Env.map (fn {global, tables, sml_tables, breakpoints} =>
   136   Env.map (fn {global, tables, sml_tables, breakpoints} =>
   116     let
   137     make_data (global, tables, bootstrap_tables sml_tables, breakpoints));
   117       val sml_tables' =
       
   118         sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
       
   119             let
       
   120               val val2 =
       
   121                 fold (fn (x, y) =>
       
   122                   member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
       
   123                 (#allVal ML_Name_Space.global ()) val1;
       
   124               val structure2 =
       
   125                 fold (fn (x, y) =>
       
   126                   member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
       
   127                 (#allStruct ML_Name_Space.global ()) structure1;
       
   128               val signature2 =
       
   129                 fold (fn (x, y) =>
       
   130                   member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
       
   131                 (#allSig ML_Name_Space.global ()) signature1;
       
   132             in (val2, type1, fixity1, structure2, signature2, functor1) end);
       
   133     in make_data (global, tables, sml_tables', breakpoints) end);
       
   134 
   138 
   135 fun set_global global =
   139 fun set_global global =
   136   Env.map (fn {tables, sml_tables, breakpoints, ...} =>
   140   Env.map (fn {tables, sml_tables, breakpoints, ...} =>
   137     make_data (global, tables, sml_tables, breakpoints));
   141     make_data (global, tables, sml_tables, breakpoints));
   138 
   142