# HG changeset patch # User wenzelm # Date 1535297318 -7200 # Node ID 78edc4bc3bd3ae0635bf1c1076f8cfd6315bd708 # Parent 10732941cc4be31211454f7e734528995d183715 clarified signature; diff -r 10732941cc4b -r 78edc4bc3bd3 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Sun Aug 26 15:39:34 2018 +0200 +++ b/src/Pure/ML/ml_env.ML Sun Aug 26 17:28:38 2018 +0200 @@ -13,8 +13,8 @@ val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit val init_bootstrap: Context.generic -> Context.generic val SML_environment: bool Config.T - val set_bootstrap: bool -> Context.generic -> Context.generic - val restore_bootstrap: Context.generic -> Context.generic -> Context.generic + val set_global: bool -> Context.generic -> Context.generic + val restore_global: Context.generic -> Context.generic -> Context.generic val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T val context: ML_Compiler0.context @@ -46,13 +46,13 @@ Symtab.merge (K true) (functor1, functor2)); type data = - {bootstrap: bool, + {global: bool, tables: tables, sml_tables: tables, breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table}; -fun make_data (bootstrap, tables, sml_tables, breakpoints) : data = - {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints}; +fun make_data (global, tables, sml_tables, breakpoints) : data = + {global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints}; structure Env = Generic_Data ( @@ -78,22 +78,22 @@ val inherit = Env.put o Env.get; fun forget_structure name = - Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + Env.map (fn {global, tables, sml_tables, breakpoints} => let - val _ = if bootstrap then ML_Name_Space.forget_structure name else (); + val _ = if global then ML_Name_Space.forget_structure name else (); val tables' = (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables); - in make_data (bootstrap, tables', sml_tables, breakpoints) end); + in make_data (global, tables', sml_tables, breakpoints) end); val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; fun add_breakpoints more_breakpoints = if is_some (Context.get_generic_context ()) then Context.>> - (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + (Env.map (fn {global, tables, sml_tables, breakpoints} => let val breakpoints' = fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints; - in make_data (bootstrap, tables, sml_tables, breakpoints') end)) + in make_data (global, tables, sml_tables, breakpoints') end)) else (); @@ -112,7 +112,7 @@ (* name space *) val init_bootstrap = - Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + Env.map (fn {global, tables, sml_tables, breakpoints} => let val sml_tables' = sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) => @@ -130,16 +130,16 @@ member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y)) (#allSig ML_Name_Space.global ()) signature1; in (val2, type1, fixity1, structure2, signature2, functor1) end); - in make_data (bootstrap, tables, sml_tables', breakpoints) end); + in make_data (global, tables, sml_tables', breakpoints) end); -fun set_bootstrap bootstrap = +fun set_global global = Env.map (fn {tables, sml_tables, breakpoints, ...} => - make_data (bootstrap, tables, sml_tables, breakpoints)); + make_data (global, tables, sml_tables, breakpoints)); -val restore_bootstrap = set_bootstrap o #bootstrap o Env.get; +val restore_global = set_global o #global o Env.get; fun add_name_space {SML} (space: ML_Name_Space.T) = - Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + Env.map (fn {global, tables, sml_tables, breakpoints} => let val (tables', sml_tables') = (tables, sml_tables) |> (if sml_env SML then apsnd else apfst) @@ -152,7 +152,7 @@ val signature2 = fold Symtab.update (#allSig space ()) signature1; val functor2 = fold Symtab.update (#allFunct space ()) functor1; in (val2, type2, fixity2, structure2, signature2, functor2) end); - in make_data (bootstrap, tables', sml_tables', breakpoints) end); + in make_data (global, tables', sml_tables', breakpoints) end); fun make_name_space {SML, exchange} : ML_Name_Space.T = let @@ -177,15 +177,15 @@ fun enter ap1 sel2 entry = if sml_env SML <> exchange then - Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} => let val sml_tables' = ap1 (Symtab.update entry) sml_tables - in make_data (bootstrap, tables, sml_tables', breakpoints) end)) + in make_data (global, tables, sml_tables', breakpoints) end)) else if is_some (Context.get_generic_context ()) then - Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} => let - val _ = if bootstrap then sel2 ML_Name_Space.global entry else (); + val _ = if global then sel2 ML_Name_Space.global entry else (); val tables' = ap1 (Symtab.update entry) tables; - in make_data (bootstrap, tables', sml_tables, breakpoints) end)) + in make_data (global, tables', sml_tables, breakpoints) end)) else sel2 ML_Name_Space.global entry; in {lookupVal = lookup #1 #lookupVal, diff -r 10732941cc4b -r 78edc4bc3bd3 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sun Aug 26 15:39:34 2018 +0200 +++ b/src/Pure/Pure.thy Sun Aug 26 17:28:38 2018 +0200 @@ -196,10 +196,10 @@ (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context - |> ML_Env.set_bootstrap true + |> ML_Env.set_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) - |> ML_Env.restore_bootstrap context + |> ML_Env.restore_global context |> Local_Theory.propagate_ml_env))); val _ =