src/Pure/Concurrent/synchronized.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 00:27:06 2014 +0200
@@ -0,0 +1,29 @@
+/*  Title:      Pure/Concurrent/synchronized.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Synchronized variables.
+*/
+
+package isabelle
+
+
+object Synchronized
+{
+  def apply[A](init: A): Synchronized[A] = new Synchronized(init)
+}
+
+
+final class Synchronized[A] private(init: A)
+{
+  private var state: A = init
+  def apply(): A = synchronized { state }
+  def >> (f: A => A) = synchronized { state = f(state) }
+  def >>>[B] (f: A => (B, A)): B = synchronized {
+    val (result, new_state) = f(state)
+    state = new_state
+    result
+  }
+
+  override def toString: String = state.toString
+}