1.1 --- a/src/Pure/context.ML	Wed Mar 26 22:40:02 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Wed Mar 26 22:40:03 2008 +0100
     1.3 @@ -63,6 +63,12 @@
     1.4    val proof_map: (generic -> generic) -> proof -> proof
     1.5    val theory_of: generic -> theory   (*total*)
     1.6    val proof_of: generic -> proof     (*total*)
     1.7 +  (*thread data*)
     1.8 +  val thread_data: unit -> generic option
     1.9 +  val the_thread_data: unit -> generic
    1.10 +  val set_thread_data: generic option -> unit
    1.11 +  val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    1.12 +  val >> : (theory -> theory) -> unit
    1.13    (*delayed setup*)
    1.14    val add_setup: (theory -> theory) -> unit
    1.15    val setup: unit -> theory -> theory
    1.16 @@ -503,6 +509,29 @@
    1.17  
    1.18  
    1.19  
    1.20 +(** thread data **)
    1.21 +
    1.22 +local val tag = Universal.tag () : generic option Universal.tag in
    1.23 +
    1.24 +fun thread_data () =
    1.25 +  (case Multithreading.get_data tag of
    1.26 +    SOME (SOME context) => SOME context
    1.27 +  | _ => NONE);
    1.28 +
    1.29 +fun the_thread_data () =
    1.30 +  (case thread_data () of
    1.31 +    SOME context => context
    1.32 +  | _ => error "Unknown context");
    1.33 +
    1.34 +fun set_thread_data context = Multithreading.put_data (tag, context);
    1.35 +fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
    1.36 +
    1.37 +fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ())));
    1.38 +
    1.39 +end;
    1.40 +
    1.41 +
    1.42 +
    1.43  (** delayed theory setup **)
    1.44  
    1.45  local