src/Pure/Concurrent/synchronized.ML

 
 signature SYNCHRONIZED =
 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;
 
 structure Synchronized: SYNCHRONIZED =

  {name = name,
   lock = Mutex.mutex (),
   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;