--- 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;