src/Pure/Concurrent/synchronized_dummy.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 32736 f126e68d003d
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
wenzelm@32736
     1
(*  Title:      Pure/Concurrent/synchronized_dummy.ML
wenzelm@32736
     2
    Author:     Makarius
wenzelm@32736
     3
wenzelm@32736
     4
Dummy version of state variables -- plain refs for sequential access.
wenzelm@32736
     5
*)
wenzelm@32736
     6
wenzelm@32736
     7
structure Synchronized: SYNCHRONIZED =
wenzelm@32736
     8
struct
wenzelm@32736
     9
wenzelm@32738
    10
datatype 'a var = Var of 'a Unsynchronized.ref;
wenzelm@32736
    11
wenzelm@32738
    12
fun var _ x = Var (Unsynchronized.ref x);
wenzelm@32736
    13
fun value (Var var) = ! var;
wenzelm@32736
    14
wenzelm@32736
    15
fun timed_access (Var var) _ f =
wenzelm@32736
    16
  (case f (! var) of
wenzelm@32736
    17
    SOME (y, x') => (var := x'; SOME y)
wenzelm@32736
    18
  | NONE => Thread.unavailable ());
wenzelm@32736
    19
wenzelm@32736
    20
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@32736
    21
wenzelm@32736
    22
fun change_result var f = guarded_access var (SOME o f);
wenzelm@32736
    23
fun change var f = change_result var (fn x => ((), f x));
wenzelm@32736
    24
wenzelm@32736
    25
end;