# HG changeset patch # User wenzelm # Date 1223982116 -7200 # Node ID 3f37ae257506a997fed449a7f2da6092586d6691 # Parent 0c50f89779716720e86eb27414c74310ba073756 added value; simplified synchronized variable access; diff -r 0c50f8977971 -r 3f37ae257506 src/Pure/Concurrent/synchronized.ML --- a/src/Pure/Concurrent/synchronized.ML Tue Oct 14 13:01:52 2008 +0200 +++ b/src/Pure/Concurrent/synchronized.ML Tue Oct 14 13:01:56 2008 +0200 @@ -9,8 +9,9 @@ sig type 'a var val var: string -> 'a -> 'a var - val guarded_change: ('a -> bool) -> ('a -> Time.time option) -> - 'a var -> (bool -> 'a -> 'b * 'a) -> 'b + val value: 'a var -> 'a + val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option + val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b val change_result: 'a var -> ('a -> 'b * 'a) -> 'b val change: 'a var -> ('a -> 'a) -> unit end; @@ -32,22 +33,35 @@ cond = ConditionVar.conditionVar (), var = ref x}; +fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var); + (* synchronized access *) -fun guarded_change guard time_limit (Var {name, lock, cond, var}) f = +fun timed_access (Var {name, lock, cond, var}) time_limit f = SimpleThread.synchronized name lock (fn () => let - fun check () = guard (! var) orelse - (case time_limit (! var) of - NONE => (ConditionVar.wait (cond, lock); check ()) - | SOME t => ConditionVar.waitUntil (cond, lock, t) andalso check ()); - val ok = check (); - val res = change_result var (f ok); + fun try_change () = + let val x = ! var in + (case f x of + SOME (y, x') => (var := x'; SOME y) + | NONE => + (case time_limit x of + NONE => (ConditionVar.wait (cond, lock); try_change ()) + | SOME t => + if ConditionVar.waitUntil (cond, lock, t) then try_change () + else NONE)) + end; + val res = try_change (); val _ = ConditionVar.broadcast cond; in res end); -fun change_result var f = guarded_change (K true) (K NONE) var (K f); +fun guarded_access var f = the (timed_access var (K NONE) f); + + +(* unconditional change *) + +fun change_result var f = guarded_access var (SOME o f); fun change var f = change_result var (fn x => ((), f x)); end;