tuned;
authorwenzelm
Mon Aug 27 15:18:18 2018 +0200 (13 months ago)
changeset 688186debac400787
parent 68817 b9568a82b474
child 68819 9cfa4aa35719
tuned;
src/Pure/ML/ml_env.ML
     1.1 --- a/src/Pure/ML/ml_env.ML	Mon Aug 27 15:01:52 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 15:18:18 2018 +0200
     1.3 @@ -21,8 +21,6 @@
     1.4    val setup: string -> theory -> theory
     1.5    val context_env: Context.generic -> string option -> string
     1.6    val default_env: string option -> string
     1.7 -  val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
     1.8 -  val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
     1.9    val forget_structure: string -> Context.generic -> Context.generic
    1.10    val bootstrap_name_space: Context.generic -> Context.generic
    1.11    val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
    1.12 @@ -30,6 +28,8 @@
    1.13    val context: ML_Compiler0.context
    1.14    val name_space: ML_Name_Space.T
    1.15    val check_functor: string -> unit
    1.16 +  val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
    1.17 +  val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
    1.18  end
    1.19  
    1.20  structure ML_Env: ML_ENV =
    1.21 @@ -93,40 +93,30 @@
    1.22  
    1.23  (* context data *)
    1.24  
    1.25 -type data =
    1.26 - {envs: tables Name_Space.table,
    1.27 -  breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
    1.28 -
    1.29 -fun make_data (envs, breakpoints) : data = {envs = envs, breakpoints = breakpoints};
    1.30 -
    1.31  structure Data = Generic_Data
    1.32  (
    1.33 -  type T = data
    1.34 -  val empty = make_data (Name_Space.empty_table "ML_environment", Inttab.empty);
    1.35 -  fun extend (data : T) = make_data (#envs data, #breakpoints data);
    1.36 -  fun merge (data : T * T) =
    1.37 -    make_data ((apply2 #envs data) |> Name_Space.join_tables (K merge_tables),
    1.38 -      Inttab.merge (K true) (apply2 #breakpoints data));
    1.39 +  type T = tables Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
    1.40 +  val empty: T = (Name_Space.empty_table "ML_environment", Inttab.empty);
    1.41 +  val extend = I;
    1.42 +  fun merge ((envs1, breakpoints1), (envs2, breakpoints2)) : T =
    1.43 +    (Name_Space.join_tables (K merge_tables) (envs1, envs2),
    1.44 +      Inttab.merge (K true) (breakpoints1, breakpoints2));
    1.45  );
    1.46  
    1.47  val inherit = Data.put o Data.get;
    1.48  
    1.49  fun setup env_name thy =
    1.50 -  thy |> (Context.theory_map o Data.map) (fn {envs, breakpoints} =>
    1.51 +  thy |> (Context.theory_map o Data.map o apfst) (fn envs =>
    1.52      let
    1.53        val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
    1.54        val tables = if env_name = Isabelle then empty_tables else sml_tables;
    1.55 -      val (_, envs') = envs
    1.56 -        |> Name_Space.define (Context.Theory thy') true (Binding.name env_name, tables);
    1.57 -    in make_data (envs', breakpoints) end);
    1.58 +    in #2 (Name_Space.define (Context.Theory thy') true (Binding.name env_name, tables) envs) end);
    1.59  
    1.60 -val get_env = Name_Space.get o #envs o Data.get;
    1.61 +val get_env = Name_Space.get o #1 o Data.get;
    1.62  
    1.63 -fun update_env env_name f context = context |> Data.map (fn {envs, breakpoints} =>
    1.64 -  let
    1.65 -    val _ = Name_Space.get envs env_name;
    1.66 -    val envs' = Name_Space.map_table_entry env_name f envs;
    1.67 -  in make_data (envs', breakpoints) end);
    1.68 +fun update_env env_name f context = context |> Data.map (apfst (fn envs =>
    1.69 +  let val _ = Name_Space.get envs env_name;
    1.70 +  in Name_Space.map_table_entry env_name f envs end));
    1.71  
    1.72  fun forget_structure name context =
    1.73    (if write_global context then ML_Name_Space.forget_structure name else ();
    1.74 @@ -264,15 +254,13 @@
    1.75  
    1.76  (* breakpoints *)
    1.77  
    1.78 -val get_breakpoint = Inttab.lookup o #breakpoints o Data.get;
    1.79 +val get_breakpoint = Inttab.lookup o #2 o Data.get;
    1.80  
    1.81  fun add_breakpoints more_breakpoints =
    1.82    if is_some (Context.get_generic_context ()) then
    1.83      Context.>>
    1.84 -      (Data.map (fn {envs, breakpoints} =>
    1.85 -        let val breakpoints' =
    1.86 -          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
    1.87 -        in make_data (envs, breakpoints') end))
    1.88 +      ((Data.map o apsnd)
    1.89 +        (fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints))
    1.90    else ();
    1.91  
    1.92  end;