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