1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/synchronized.ML	Mon Oct 13 15:48:40 2008 +0200
     1.3 @@ -0,0 +1,53 @@
     1.4 +(*  Title:      Pure/Concurrent/synchronized.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Fabian Immler and Makarius
     1.7 +
     1.8 +State variables with synchronized access.
     1.9 +*)
    1.10 +
    1.11 +signature SYNCHRONIZED =
    1.12 +sig
    1.13 +  type 'a var
    1.14 +  val var: string -> 'a -> 'a var
    1.15 +  val guarded_change: ('a -> bool) -> ('a -> Time.time option) ->
    1.16 +    'a var -> (bool -> 'a -> 'b * 'a) -> 'b
    1.17 +  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
    1.18 +  val change: 'a var -> ('a -> 'a) -> unit
    1.19 +end;
    1.20 +
    1.21 +structure Synchronized: SYNCHRONIZED =
    1.22 +struct
    1.23 +
    1.24 +(* state variables *)
    1.25 +
    1.26 +datatype 'a var = Var of
    1.27 + {name: string,
    1.28 +  lock: Mutex.mutex,
    1.29 +  cond: ConditionVar.conditionVar,
    1.30 +  var: 'a ref};
    1.31 +
    1.32 +fun var name x = Var
    1.33 + {name = name,
    1.34 +  lock = Mutex.mutex (),
    1.35 +  cond = ConditionVar.conditionVar (),
    1.36 +  var = ref x};
    1.37 +
    1.38 +
    1.39 +(* synchronized access *)
    1.40 +
    1.41 +fun guarded_change guard time_limit (Var {name, lock, cond, var}) f =
    1.42 +  SimpleThread.synchronized name lock (fn () =>
    1.43 +    let
    1.44 +      fun check () = guard (! var) orelse
    1.45 +        (case time_limit (! var) of
    1.46 +          NONE => (ConditionVar.wait (cond, lock); check ())
    1.47 +        | SOME t => ConditionVar.waitUntil (cond, lock, t) andalso check ());
    1.48 +      val ok = check ();
    1.49 +      val res = change_result var (f ok);
    1.50 +      val _ = ConditionVar.broadcast cond;
    1.51 +    in res end);
    1.52 +
    1.53 +fun change_result var f = guarded_change (K true) (K NONE) var (K f);
    1.54 +fun change var f = change_result var (fn x => ((), f x));
    1.55 +
    1.56 +end;