equal
deleted
inserted
replaced
|
1 (* Title: Pure/Concurrent/thread_data_virtual.ML |
|
2 Author: Makarius |
|
3 |
|
4 Thread-local data -- virtual version with context management. |
|
5 *) |
|
6 |
|
7 structure Thread_Data_Virtual: THREAD_DATA = |
|
8 struct |
|
9 |
|
10 (* context data *) |
|
11 |
|
12 structure Data = Generic_Data |
|
13 ( |
|
14 type T = Universal.universal Inttab.table; |
|
15 val empty = Inttab.empty; |
|
16 val extend = I; |
|
17 val merge = Inttab.merge (K true); |
|
18 ); |
|
19 |
|
20 abstype 'a var = Var of serial * 'a Universal.tag |
|
21 with |
|
22 |
|
23 fun var () : 'a var = Var (serial (), Universal.tag ()); |
|
24 |
|
25 fun get (Var (i, tag)) = |
|
26 Inttab.lookup (Data.get (Context.the_generic_context ())) i |
|
27 |> Option.map (Universal.tagProject tag); |
|
28 |
|
29 fun put (Var (i, tag)) data = |
|
30 (Context.>> o Data.map) |
|
31 (case data of |
|
32 NONE => Inttab.delete_safe i |
|
33 | SOME x => Inttab.update (i, Universal.tagInject tag x)); |
|
34 |
|
35 fun setmp v data f x = |
|
36 Multithreading.uninterruptible (fn restore_attributes => fn () => |
|
37 let |
|
38 val orig_data = get v; |
|
39 val _ = put v data; |
|
40 val result = Exn.capture (restore_attributes f) x; |
|
41 val _ = put v orig_data; |
|
42 in Exn.release result end) (); |
|
43 |
|
44 end; |
|
45 |
|
46 val is_virtual = true; |
|
47 |
|
48 end; |