# HG changeset patch
# User wenzelm
# Date 1398334195 -7200
# Node ID 8219a65b24e33d6eda6d12ec7d156fb155226123
# Parent  ad5d7461b370cc2016c5320b35aecde42c02988d
synchronized access, similar to ML version;

diff -r ad5d7461b370 -r 8219a65b24e3 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 11:01:14 2014 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 12:09:55 2014 +0200
@@ -18,7 +18,7 @@
 structure Synchronized: SYNCHRONIZED =
 struct
 
-(* state variables *)
+(* state variable *)
 
 abstype 'a var = Var of
  {name: string,
diff -r ad5d7461b370 -r 8219a65b24e3 src/Pure/Concurrent/synchronized.scala
--- a/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 11:01:14 2014 +0200
+++ b/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 12:09:55 2014 +0200
@@ -8,6 +8,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
+
+
 object Synchronized
 {
   def apply[A](init: A): Synchronized[A] = new Synchronized(init)
@@ -16,14 +19,59 @@
 
 final class Synchronized[A] private(init: A)
 {
+  /* state variable */
+
   private var state: A = init
+
   def value: A = synchronized { state }
+  override def toString: String = value.toString
+
+
+  /* synchronized access */
+
+  def timed_access[B](time_limit: A => Option[Time], f: A => Option[(B, A)]): Option[B] =
+    synchronized {
+      def check(x: A): Option[B] =
+        f(x) match {
+          case None => None
+          case Some((y, x1)) =>
+            state = x1
+            notifyAll()
+            Some(y)
+        }
+      @tailrec def try_change(): Option[B] =
+      {
+        val x = state
+        check(x) match {
+          case None =>
+            time_limit(x) match {
+              case Some(t) =>
+                val timeout = (t - Time.now()).ms
+                if (timeout > 0L) {
+                  wait(timeout)
+                  check(state)
+                }
+                else None
+              case None =>
+                wait()
+                try_change()
+            }
+          case some => some
+        }
+      }
+      try_change()
+    }
+
+  def guarded_access[B](f: A => Option[(B, A)]): B =
+    timed_access(_ => None, f).get
+
+
+  /* unconditional change */
+
   def change(f: A => A) = synchronized { state = f(state) }
   def change_result[B](f: A => (B, A)): B = synchronized {
     val (result, new_state) = f(state)
     state = new_state
     result
   }
-
-  override def toString: String = state.toString
 }