src/Pure/Concurrent/thread_data.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -0,0 +1,42 @@
+(*  Title:      Pure/Concurrent/thread_data.ML
+    Author:     Makarius
+
+Thread-local data -- raw version without context management.
+*)
+
+signature THREAD_DATA =
+sig
+  type 'a var
+  val var: unit -> 'a var
+  val get: 'a var -> 'a option
+  val put: 'a var -> 'a option -> unit
+  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
+end;
+
+structure Thread_Data: THREAD_DATA =
+struct
+
+abstype 'a var = Var of 'a option Universal.tag
+with
+
+fun var () : 'a var = Var (Universal.tag ());
+
+fun get (Var tag) =
+  (case Thread.getLocal tag of
+    SOME data => data
+  | NONE => NONE);
+
+fun put (Var tag) data = Thread.setLocal (tag, data);
+
+fun setmp v data f x =
+  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;
+
+end;