tuned signature;
authorwenzelm
Tue Aug 28 11:22:04 2018 +0200 (14 months ago)
changeset 688271286ca9dfd26
parent 68826 deefe5837120
child 68828 7030922e91a1
tuned signature;
src/Pure/Pure.thy
src/Pure/config.ML
     1.1 --- a/src/Pure/Pure.thy	Tue Aug 28 11:13:33 2018 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Aug 28 11:22:04 2018 +0200
     1.3 @@ -200,10 +200,8 @@
     1.4          |> Config.put_generic ML_Env.ML_write_global true
     1.5          |> ML_Context.exec (fn () =>
     1.6              ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
     1.7 -        |> Config.put_generic ML_Env.ML_write_global
     1.8 -            (Config.get_generic context ML_Env.ML_write_global)
     1.9 -        |> Config.put_generic ML_Env.ML_environment
    1.10 -            (Config.get_generic context ML_Env.ML_environment)
    1.11 +        |> Config.restore_generic ML_Env.ML_write_global context
    1.12 +        |> Config.restore_generic ML_Env.ML_environment context
    1.13          |> Local_Theory.propagate_ml_env)));
    1.14  
    1.15  val _ =
     2.1 --- a/src/Pure/config.ML	Tue Aug 28 11:13:33 2018 +0200
     2.2 +++ b/src/Pure/config.ML	Tue Aug 28 11:22:04 2018 +0200
     2.3 @@ -18,12 +18,15 @@
     2.4    val get: Proof.context -> 'a T -> 'a
     2.5    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
     2.6    val put: 'a T -> 'a -> Proof.context -> Proof.context
     2.7 +  val restore: 'a T -> Proof.context -> Proof.context -> Proof.context
     2.8    val get_global: theory -> 'a T -> 'a
     2.9    val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    2.10    val put_global: 'a T -> 'a -> theory -> theory
    2.11 +  val restore_global: 'a T -> theory -> theory -> theory
    2.12    val get_generic: Context.generic -> 'a T -> 'a
    2.13    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    2.14    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    2.15 +  val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
    2.16    val declare: string * Position.T -> (Context.generic -> value) -> raw
    2.17    val declare_option: string * Position.T -> raw
    2.18    val name_of: 'a T -> string
    2.19 @@ -91,14 +94,17 @@
    2.20  fun get_generic context (Config {get_value, ...}) = get_value context;
    2.21  fun map_generic (Config {map_value, ...}) f context = map_value f context;
    2.22  fun put_generic config value = map_generic config (K value);
    2.23 +fun restore_generic config context = put_generic config (get_generic context config);
    2.24  
    2.25  fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    2.26  fun map_ctxt config f = Context.proof_map (map_generic config f);
    2.27  fun put_ctxt config value = map_ctxt config (K value);
    2.28 +fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config);
    2.29  
    2.30  fun get_global thy = get_generic (Context.Theory thy);
    2.31  fun map_global config f = Context.theory_map (map_generic config f);
    2.32  fun put_global config value = map_global config (K value);
    2.33 +fun restore_global config thy = put_global config (get_global thy config);
    2.34  
    2.35  
    2.36  (* context information *)
    2.37 @@ -145,5 +151,6 @@
    2.38  val get = get_ctxt;
    2.39  val map = map_ctxt;
    2.40  val put = put_ctxt;
    2.41 +val restore = restore_ctxt;
    2.42  
    2.43  end;