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