src/Pure/ML-Systems/unsynchronized.ML
author blanchet
Wed, 02 Jun 2010 15:18:48 +0200
changeset 37321 9d7cfae95b30
parent 32737 76fa673eee8b
child 38799 712cb964d113
permissions -rw-r--r--
honor "xsymbols"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32737
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/unsynchronized.ML
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     3
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     4
Raw ML references as unsynchronized state variables.
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     5
*)
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     6
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     7
structure Unsynchronized =
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     8
struct
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
     9
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    10
datatype ref = datatype ref;
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    11
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    12
val op := = op :=;
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    13
val ! = !;
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    14
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    15
fun set flag = (flag := true; true);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    16
fun reset flag = (flag := false; false);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    17
fun toggle flag = (flag := not (! flag); ! flag);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    18
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    19
fun change r f = r := f (! r);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    20
fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    21
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    22
fun inc i = (i := ! i + (1: int); ! i);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    23
fun dec i = (i := ! i - (1: int); ! i);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    24
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    25
end;