author | wenzelm |
Thu, 03 Mar 2016 21:59:21 +0100 | |
changeset 62508 | d0b68218ea55 |
parent 61925 | src/Pure/RAW/unsynchronized.ML@ab52f183f020 |
child 62818 | 2733b240bfea |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
61925
diff
changeset
|
1 |
(* Title: Pure/Concurrent/unsynchronized.ML |
32737 | 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 |
||
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
21 |
fun setmp flag value f x = |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
22 |
uninterruptible (fn restore_attributes => fn () => |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
23 |
let |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
24 |
val orig_value = ! flag; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
25 |
val _ = flag := value; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
26 |
val result = Exn.capture (restore_attributes f) x; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
27 |
val _ = flag := orig_value; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
28 |
in Exn.release result end) (); |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38799
diff
changeset
|
29 |
|
32737 | 30 |
end; |