equal
deleted
inserted
replaced
|
1 (* Title: Pure/Concurrent/unsynchronized.ML |
|
2 Author: Makarius |
|
3 |
|
4 Raw ML references as unsynchronized state variables. |
|
5 *) |
|
6 |
|
7 structure Unsynchronized = |
|
8 struct |
|
9 |
|
10 datatype ref = datatype ref; |
|
11 |
|
12 val op := = op :=; |
|
13 val ! = !; |
|
14 |
|
15 fun change r f = r := f (! r); |
|
16 fun change_result r f = let val (x, y) = f (! r) in r := y; x end; |
|
17 |
|
18 fun inc i = (i := ! i + (1: int); ! i); |
|
19 fun dec i = (i := ! i - (1: int); ! i); |
|
20 |
|
21 fun setmp flag value f x = |
|
22 uninterruptible (fn restore_attributes => fn () => |
|
23 let |
|
24 val orig_value = ! flag; |
|
25 val _ = flag := value; |
|
26 val result = Exn.capture (restore_attributes f) x; |
|
27 val _ = flag := orig_value; |
|
28 in Exn.release result end) (); |
|
29 |
|
30 end; |