added setmp_thread_data;
authorwenzelm
Thu Jan 03 00:15:39 2008 +0100 (2008-01-03)
changeset 25797b293e3ed3cad
parent 25796 5df3607867c1
child 25798 1e6eafbb466f
added setmp_thread_data;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Jan 02 23:00:57 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Jan 03 00:15:39 2008 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    val change: 'a ref -> ('a -> 'a) -> unit
     1.5    val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.6    val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.7 +  val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.8  
     1.9    (*lists*)
    1.10    exception UnequalLengths
    1.11 @@ -338,6 +339,13 @@
    1.12  
    1.13  fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
    1.14  
    1.15 +fun setmp_thread_data tag orig_data data f x =
    1.16 +  let
    1.17 +    val _ = Multithreading.put_data (tag, data);
    1.18 +    val result = Exn.capture f x;
    1.19 +    val _ = Multithreading.put_data (tag, orig_data);
    1.20 +  in Exn.release result end;
    1.21 +
    1.22  
    1.23  
    1.24  (** lists **)