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