# HG changeset patch
# User wenzelm
# Date 1206567603 -3600
# Node ID 003dd6155870f1f4148776a11a3b58eb1ce5d0c0
# Parent  0918f5c0bbcaa717e64f10e72256c60258b28832
added thread data (formerly global ref in ML/ml_context.ML);
renamed ML_Context.>> to Context.>> (again);

diff -r 0918f5c0bbca -r 003dd6155870 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Mar 26 22:40:02 2008 +0100
+++ b/src/Pure/context.ML	Wed Mar 26 22:40:03 2008 +0100
@@ -63,6 +63,12 @@
   val proof_map: (generic -> generic) -> proof -> proof
   val theory_of: generic -> theory   (*total*)
   val proof_of: generic -> proof     (*total*)
+  (*thread data*)
+  val thread_data: unit -> generic option
+  val the_thread_data: unit -> generic
+  val set_thread_data: generic option -> unit
+  val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
+  val >> : (theory -> theory) -> unit
   (*delayed setup*)
   val add_setup: (theory -> theory) -> unit
   val setup: unit -> theory -> theory
@@ -503,6 +509,29 @@
 
 
 
+(** thread data **)
+
+local val tag = Universal.tag () : generic option Universal.tag in
+
+fun thread_data () =
+  (case Multithreading.get_data tag of
+    SOME (SOME context) => SOME context
+  | _ => NONE);
+
+fun the_thread_data () =
+  (case thread_data () of
+    SOME context => context
+  | _ => error "Unknown context");
+
+fun set_thread_data context = Multithreading.put_data (tag, context);
+fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+
+fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ())));
+
+end;
+
+
+
 (** delayed theory setup **)
 
 local