1(*  Title:      Pure/Concurrent/thread_data.ML
2    Author:     Makarius
3
4Thread-local data -- physical version without context management.
5*)
6
7signature THREAD_DATA =
8sig
9  type 'a var
10  val var: unit -> 'a var
11  val get: 'a var -> 'a option
12  val put: 'a var -> 'a option -> unit
13  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
14  val is_virtual: bool
15end;
16
17structure Thread_Data: THREAD_DATA =
18struct
19
20abstype 'a var = Var of 'a option Universal.tag
21with
22
23fun var () : 'a var = Var (Universal.tag ());
24
25fun get (Var tag) =
26  (case Thread.Thread.getLocal tag of
27    SOME data => data
28  | NONE => NONE);
29
30fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
31
32fun setmp v data f x =
33  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
34    let
35      val orig_data = get v;
36      val _ = put v data;
37      val result = Exn.capture (restore_attributes f) x;
38      val _ = put v orig_data;
39    in Exn.release result end) ();
40
41end;
42
43val is_virtual = false;
44
45end;
46