1/* Title: Pure/Concurrent/synchronized.scala 2 Author: Makarius 3 4Synchronized variables. 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11 12 13object Synchronized 14{ 15 def apply[A](init: A): Synchronized[A] = new Synchronized(init) 16} 17 18 19final class Synchronized[A] private(init: A) 20{ 21 /* state variable */ 22 23 private var state: A = init 24 25 def value: A = synchronized { state } 26 override def toString: String = value.toString 27 28 29 /* synchronized access */ 30 31 def timed_access[B](time_limit: A => Option[Time], f: A => Option[(B, A)]): Option[B] = 32 synchronized { 33 def check(x: A): Option[B] = 34 f(x) match { 35 case None => None 36 case Some((y, x1)) => 37 state = x1 38 notifyAll() 39 Some(y) 40 } 41 @tailrec def try_change(): Option[B] = 42 { 43 val x = state 44 check(x) match { 45 case None => 46 time_limit(x) match { 47 case Some(t) => 48 val timeout = (t - Time.now()).ms 49 if (timeout > 0L) { 50 wait(timeout) 51 check(state) 52 } 53 else None 54 case None => 55 wait() 56 try_change() 57 } 58 case some => some 59 } 60 } 61 try_change() 62 } 63 64 def guarded_access[B](f: A => Option[(B, A)]): B = 65 timed_access(_ => None, f).get 66 67 68 /* unconditional change */ 69 70 def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() } 71 72 def change_result[B](f: A => (B, A)): B = synchronized { 73 val (result, new_state) = f(state) 74 state = new_state 75 notifyAll() 76 result 77 } 78} 79