src/Pure/context.ML
changeset 62889 99c7f31615c2
parent 62876 507c90523113
child 65459 da59e8e0a663
     1.1 --- a/src/Pure/context.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -73,9 +73,9 @@
     1.4    val theory_of: generic -> theory  (*total*)
     1.5    val proof_of: generic -> Proof.context  (*total*)
     1.6    (*thread data*)
     1.7 -  val thread_data: unit -> generic option
     1.8 -  val set_thread_data: generic option -> unit
     1.9 -  val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    1.10 +  val get_generic_context: unit -> generic option
    1.11 +  val put_generic_context: generic option -> unit
    1.12 +  val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b
    1.13    val the_generic_context: unit -> generic
    1.14    val the_global_context: unit -> theory
    1.15    val the_local_context: unit -> Proof.context
    1.16 @@ -491,18 +491,14 @@
    1.17  
    1.18  (** thread data **)
    1.19  
    1.20 -local val tag = Universal.tag () : generic option Universal.tag in
    1.21 +local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in
    1.22  
    1.23 -fun thread_data () =
    1.24 -  (case Thread.getLocal tag of
    1.25 -    SOME (SOME context) => SOME context
    1.26 -  | _ => NONE);
    1.27 -
    1.28 -fun set_thread_data context = Thread.setLocal (tag, context);
    1.29 -fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
    1.30 +fun get_generic_context () = Thread_Data.get generic_context_var;
    1.31 +val put_generic_context = Thread_Data.put generic_context_var;
    1.32 +fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context;
    1.33  
    1.34  fun the_generic_context () =
    1.35 -  (case thread_data () of
    1.36 +  (case get_generic_context () of
    1.37      SOME context => context
    1.38    | _ => error "Unknown context");
    1.39  
    1.40 @@ -514,13 +510,13 @@
    1.41  fun >>> f =
    1.42    let
    1.43      val (res, context') = f (the_generic_context ());
    1.44 -    val _ = set_thread_data (SOME context');
    1.45 +    val _ = put_generic_context (SOME context');
    1.46    in res end;
    1.47  
    1.48  nonfix >>;
    1.49  fun >> f = >>> (fn context => ((), f context));
    1.50  
    1.51 -val _ = set_thread_data (SOME (Theory pre_pure_thy));
    1.52 +val _ = put_generic_context (SOME (Theory pre_pure_thy));
    1.53  
    1.54  end;
    1.55