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