src/Pure/Concurrent/synchronized_sequential.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32816 5db89f8d44f3
child 33060 e66b41782cb5
permissions -rw-r--r--
map_range (and map_index) combinator
     1 (*  Title:      Pure/Concurrent/synchronized_sequential.ML
     2     Author:     Makarius
     3 
     4 Sequential version of state variables -- plain refs.
     5 *)
     6 
     7 structure Synchronized: SYNCHRONIZED =
     8 struct
     9 
    10 abstype 'a var = Var of 'a Unsynchronized.ref
    11 with
    12 
    13 fun var _ x = Var (Unsynchronized.ref x);
    14 fun value (Var var) = ! var;
    15 
    16 fun timed_access (Var var) _ f =
    17   (case f (! var) of
    18     SOME (y, x') => (var := x'; SOME y)
    19   | NONE => Thread.unavailable ());
    20 
    21 fun guarded_access var f = the (timed_access var (K NONE) f);
    22 
    23 fun change_result var f = guarded_access var (SOME o f);
    24 fun change var f = change_result var (fn x => ((), f x));
    25 
    26 end;
    27 end;