# HG changeset patch
# User wenzelm
# Date 1398292026 -7200
# Node ID 535d59d4ed12b21b7c87595f75a2d31fd922103e
# Parent  660ffb5260696c3ac459776886c200b11126f3b6
more uniform synchronized variables;

diff -r 660ffb526069 -r 535d59d4ed12 src/Pure/Concurrent/counter.scala
--- a/src/Pure/Concurrent/counter.scala	Wed Apr 23 17:57:56 2014 +0200
+++ b/src/Pure/Concurrent/counter.scala	Thu Apr 24 00:27:06 2014 +0200
@@ -25,5 +25,7 @@
     count -= 1
     count
   }
+
+  override def toString: String = count.toString
 }
 
diff -r 660ffb526069 -r 535d59d4ed12 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Wed Apr 23 17:57:56 2014 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 00:27:06 2014 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Concurrent/synchronized.ML
     Author:     Fabian Immler and Makarius
 
-State variables with synchronized access.
+Synchronized variables.
 *)
 
 signature SYNCHRONIZED =
diff -r 660ffb526069 -r 535d59d4ed12 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
+}
diff -r 660ffb526069 -r 535d59d4ed12 src/Pure/Concurrent/volatile.scala
--- a/src/Pure/Concurrent/volatile.scala	Wed Apr 23 17:57:56 2014 +0200
+++ b/src/Pure/Concurrent/volatile.scala	Thu Apr 24 00:27:06 2014 +0200
@@ -25,5 +25,7 @@
     state = new_state
     result
   }
+
+  override def toString: String = state.toString
 }
 
diff -r 660ffb526069 -r 535d59d4ed12 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Apr 23 17:57:56 2014 +0200
+++ b/src/Pure/build-jars	Thu Apr 24 00:27:06 2014 +0200
@@ -12,6 +12,7 @@
   Concurrent/counter.scala
   Concurrent/future.scala
   Concurrent/simple_thread.scala
+  Concurrent/synchronized.scala
   Concurrent/volatile.scala
   General/antiquote.scala
   General/bytes.scala