author  wenzelm 
Wed, 22 Sep 2010 18:21:48 +0200  
changeset 39616  8052101883c3 
parent 38799  712cb964d113 
permissions  rwrr 
32737  1 
(* Title: Pure/MLSystems/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 

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; 