src/Pure/ML/ml_env.ML
changeset 68865 dd44e31ca2c6
parent 68823 5e7b1ae10eb8
child 68917 75691a5c8fb6
     1.1 --- a/src/Pure/ML/ml_env.ML	Fri Aug 31 16:17:30 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Fri Aug 31 22:25:58 2018 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val ML_read_global: bool Config.T
     1.5    val ML_write_global_raw: Config.raw
     1.6    val ML_write_global: bool Config.T
     1.7 -  val inherit: Context.generic -> Context.generic -> Context.generic
     1.8 +  val inherit: Context.generic list -> Context.generic -> Context.generic
     1.9    type operations =
    1.10     {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
    1.11      explode_token: ML_Lex.token -> char list}
    1.12 @@ -101,20 +101,31 @@
    1.13   {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
    1.14    explode_token: ML_Lex.token -> char list};
    1.15  
    1.16 +local
    1.17 +
    1.18  type env = tables * operations;
    1.19 +type data = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
    1.20 +
    1.21 +val empty_data: data = (Name_Space.empty_table "ML_environment", Inttab.empty);
    1.22 +
    1.23 +fun merge_data ((envs1, breakpoints1), (envs2, breakpoints2)) : data =
    1.24 +  ((envs1, envs2) |> Name_Space.join_tables
    1.25 +    (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
    1.26 +   Inttab.merge (K true) (breakpoints1, breakpoints2));
    1.27 +
    1.28 +in
    1.29  
    1.30  structure Data = Generic_Data
    1.31  (
    1.32 -  type T = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
    1.33 -  val empty: T = (Name_Space.empty_table "ML_environment", Inttab.empty);
    1.34 +  type T = data;
    1.35 +  val empty = empty_data;
    1.36    val extend = I;
    1.37 -  fun merge ((envs1, breakpoints1), (envs2, breakpoints2)) : T =
    1.38 -    ((envs1, envs2) |> Name_Space.join_tables
    1.39 -      (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
    1.40 -     Inttab.merge (K true) (breakpoints1, breakpoints2));
    1.41 +  val merge = merge_data;
    1.42  );
    1.43  
    1.44 -val inherit = Data.put o Data.get;
    1.45 +fun inherit contexts = Data.put (Library.foldl1 merge_data (map Data.get contexts));
    1.46 +
    1.47 +end;
    1.48  
    1.49  val get_env = Name_Space.get o #1 o Data.get;
    1.50  val get_tables = #1 oo get_env;