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