src/Pure/Concurrent/synchronized.scala
author wenzelm
Mon Oct 24 12:16:12 2016 +0200 (2016-10-24)
changeset 64370 865b39487b5d
parent 56694 c4e77643aad6
permissions -rw-r--r--
discontinued unused / untested distinction of separate PIDE modules;
     1 /*  Title:      Pure/Concurrent/synchronized.scala
     2     Author:     Makarius
     3 
     4 Synchronized variables.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 
    12 
    13 object Synchronized
    14 {
    15   def apply[A](init: A): Synchronized[A] = new Synchronized(init)
    16 }
    17 
    18 
    19 final 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 }