# HG changeset patch
# User wenzelm
# Date 1198181522 -3600
# Node ID 4d147263f71fcc9b456d4fab9e0762a9031d8ff5
# Parent  b00b903ae8aee4a33eb54bd0785fa8764b566769
added get/put_data;

diff -r b00b903ae8ae -r 4d147263f71f src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Thu Dec 20 21:12:01 2007 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Thu Dec 20 21:12:02 2007 +0100
@@ -23,29 +23,66 @@
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
   val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
   val serial: unit -> int
+  val get_data: 'a Universal.tag -> 'a option
+  val put_data: 'a Universal.tag * 'a -> unit
 end;
 
 structure Multithreading: MULTITHREADING =
 struct
 
+(* options *)
+
 val trace = ref (0: int);
 fun tracing _ _ = ();
 
 val available = false;
 val max_threads = ref (1: int);
 
+
+(* critical section *)
+
 fun self_critical () = false;
 fun NAMED_CRITICAL _ e = e ();
 fun CRITICAL e = e ();
 
+
+(* scheduling *)
+
 datatype 'a task =
   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
 
 fun schedule _ _ _ = raise Fail "No multithreading support";
 
+
+(* serial numbers *)
+
 local val count = ref (0: int)
 in fun serial () = (count := ! count + 1; ! count) end;
 
+
+(* thread data *)
+
+local
+
+val data = ref ([]: Universal.universal ref list);
+
+fun find_data tag =
+  let
+    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
+      | find [] = NONE;
+  in find (! data) end;
+
+in
+
+fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
+
+fun put_data (tag, x) =
+  (case find_data tag of
+    SOME r => r := Universal.tagInject tag x
+  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
+
+end;
+
 end;
 
 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
diff -r b00b903ae8ae -r 4d147263f71f src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:01 2007 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 20 21:12:02 2007 +0100
@@ -257,6 +257,12 @@
 
 end;
 
+
+(* thread data *)
+
+val get_data = Thread.getLocal;
+val put_data = Thread.setLocal;
+
 end;
 
 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;