src/Pure/Concurrent/synchronized.scala
author wenzelm
Thu, 24 Apr 2014 00:27:06 +0200
changeset 56685 535d59d4ed12
child 56687 7fb98325722a
permissions -rw-r--r--
more uniform synchronized variables;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56685
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/synchronized.scala
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     2
    Module:     PIDE
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     4
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     5
Synchronized variables.
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     6
*/
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     7
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     8
package isabelle
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
     9
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    10
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    11
object Synchronized
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    12
{
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    13
  def apply[A](init: A): Synchronized[A] = new Synchronized(init)
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    14
}
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    15
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    16
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    17
final class Synchronized[A] private(init: A)
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    18
{
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    19
  private var state: A = init
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    20
  def apply(): A = synchronized { state }
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    21
  def >> (f: A => A) = synchronized { state = f(state) }
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    22
  def >>>[B] (f: A => (B, A)): B = synchronized {
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    23
    val (result, new_state) = f(state)
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    24
    state = new_state
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    25
    result
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    26
  }
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    27
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    28
  override def toString: String = state.toString
535d59d4ed12 more uniform synchronized variables;
wenzelm
parents:
diff changeset
    29
}