src/Pure/ML-Systems/unsynchronized.ML
author wenzelm
Tue Sep 29 11:48:32 2009 +0200 (2009-09-29)
changeset 32737 76fa673eee8b
child 38799 712cb964d113
permissions -rw-r--r--
Raw ML references as unsynchronized state variables.
wenzelm@32737
     1
(*  Title:      Pure/ML-Systems/unsynchronized.ML
wenzelm@32737
     2
    Author:     Makarius
wenzelm@32737
     3
wenzelm@32737
     4
Raw ML references as unsynchronized state variables.
wenzelm@32737
     5
*)
wenzelm@32737
     6
wenzelm@32737
     7
structure Unsynchronized =
wenzelm@32737
     8
struct
wenzelm@32737
     9
wenzelm@32737
    10
datatype ref = datatype ref;
wenzelm@32737
    11
wenzelm@32737
    12
val op := = op :=;
wenzelm@32737
    13
val ! = !;
wenzelm@32737
    14
wenzelm@32737
    15
fun set flag = (flag := true; true);
wenzelm@32737
    16
fun reset flag = (flag := false; false);
wenzelm@32737
    17
fun toggle flag = (flag := not (! flag); ! flag);
wenzelm@32737
    18
wenzelm@32737
    19
fun change r f = r := f (! r);
wenzelm@32737
    20
fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
wenzelm@32737
    21
wenzelm@32737
    22
fun inc i = (i := ! i + (1: int); ! i);
wenzelm@32737
    23
fun dec i = (i := ! i - (1: int); ! i);
wenzelm@32737
    24
wenzelm@32737
    25
end;