src/Pure/ML-Systems/unsynchronized.ML
changeset 32737 76fa673eee8b
child 38799 712cb964d113
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/unsynchronized.ML	Tue Sep 29 11:48:32 2009 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Title:      Pure/ML-Systems/unsynchronized.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Raw ML references as unsynchronized state variables.
     1.8 +*)
     1.9 +
    1.10 +structure Unsynchronized =
    1.11 +struct
    1.12 +
    1.13 +datatype ref = datatype ref;
    1.14 +
    1.15 +val op := = op :=;
    1.16 +val ! = !;
    1.17 +
    1.18 +fun set flag = (flag := true; true);
    1.19 +fun reset flag = (flag := false; false);
    1.20 +fun toggle flag = (flag := not (! flag); ! flag);
    1.21 +
    1.22 +fun change r f = r := f (! r);
    1.23 +fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
    1.24 +
    1.25 +fun inc i = (i := ! i + (1: int); ! i);
    1.26 +fun dec i = (i := ! i - (1: int); ! i);
    1.27 +
    1.28 +end;