--- a/src/Pure/library.ML Wed Jan 02 23:00:57 2008 +0100
+++ b/src/Pure/library.ML Thu Jan 03 00:15:39 2008 +0100
@@ -65,6 +65,7 @@
val change: 'a ref -> ('a -> 'a) -> unit
val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+ val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
(*lists*)
exception UnequalLengths
@@ -338,6 +339,13 @@
fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
+fun setmp_thread_data tag orig_data data f x =
+ let
+ val _ = Multithreading.put_data (tag, data);
+ val result = Exn.capture f x;
+ val _ = Multithreading.put_data (tag, orig_data);
+ in Exn.release result end;
+
(** lists **)