src/Pure/ML/ml_env.ML
changeset 68276 cbee43ff4ceb
parent 64556 851ae0e7b09c
child 68813 78edc4bc3bd3
     1.1 --- a/src/Pure/ML/ml_env.ML	Fri May 25 22:47:36 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Fri May 25 22:47:57 2018 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
     1.5    val init_bootstrap: Context.generic -> Context.generic
     1.6    val SML_environment: bool Config.T
     1.7 +  val set_bootstrap: bool -> Context.generic -> Context.generic
     1.8 +  val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
     1.9    val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
    1.10    val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    1.11    val context: ML_Compiler0.context
    1.12 @@ -130,6 +132,12 @@
    1.13              in (val2, type1, fixity1, structure2, signature2, functor1) end);
    1.14      in make_data (bootstrap, tables, sml_tables', breakpoints) end);
    1.15  
    1.16 +fun set_bootstrap bootstrap =
    1.17 +  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
    1.18 +    make_data (bootstrap, tables, sml_tables, breakpoints));
    1.19 +
    1.20 +val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
    1.21 +
    1.22  fun add_name_space {SML} (space: ML_Name_Space.T) =
    1.23    Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    1.24      let