src/Pure/ML-Systems/unsynchronized.ML
author wenzelm
Wed, 22 Sep 2010 18:21:48 +0200
changeset 39616 8052101883c3
parent 38799 712cb964d113
permissions -rw-r--r--
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
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 change r f = r := f (! r);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    16
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
    17
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    18
fun inc i = (i := ! i + (1: int); ! i);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    19
fun dec i = (i := ! i - (1: int); ! i);
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    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
76fa673eee8b Raw ML references as unsynchronized state variables.
wenzelm
parents:
diff changeset
    30
end;