virtual thread data via context, for proper support of Context.>> etc;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_data_virtual.ML	Wed Apr 06 19:03:29 2016 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Pure/Concurrent/thread_data_virtual.ML
+    Author:     Makarius
+
+Thread-local data -- virtual version with context management.
+*)
+
+structure Thread_Data_Virtual: THREAD_DATA =
+struct
+
+(* context data *)
+
+structure Data = Generic_Data
+(
+  type T = Universal.universal Inttab.table;
+  val empty = Inttab.empty;
+  val extend = I;
+  val merge = Inttab.merge (K true);
+);
+
+abstype 'a var = Var of serial * 'a Universal.tag
+with
+
+fun var () : 'a var = Var (serial (), Universal.tag ());
+
+fun get (Var (i, tag)) =
+  Inttab.lookup (Data.get (Context.the_generic_context ())) i
+  |> Option.map (Universal.tagProject tag);
+
+fun put (Var (i, tag)) data =
+  (Context.>> o Data.map)
+    (case data of
+      NONE => Inttab.delete_safe i
+    | SOME x => Inttab.update (i, Universal.tagInject tag x));
+
+fun setmp v data f x =
+  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_data = get v;
+      val _ = put v data;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = put v orig_data;
+    in Exn.release result end) ();
+
+end;
+
+val is_virtual = true;
+
+end;

--- a/src/Pure/ML_Bootstrap.thy	Wed Apr 06 17:17:05 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Wed Apr 06 19:03:29 2016 +0200
@@ -10,6 +10,7 @@
 begin
 
 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
+SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
 
 ML \<open>
 local

--- a/src/Pure/ROOT.ML	Wed Apr 06 17:17:05 2016 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 06 19:03:29 2016 +0200
@@ -99,6 +99,7 @@
 
 use "ML/ml_statistics.ML";
 
+use "Concurrent/thread_data_virtual.ML";
 use "Concurrent/standard_thread.ML";
 use "Concurrent/single_assignment.ML";