# HG changeset patch
# User wenzelm
# Date 1283008853 -7200
# Node ID ec75dc58688b4cd813ef9b0b38acce1b61afa365
# Parent  be9dace0ff58742a57a29b67bc728d9fa8cbe1bc
volatile variables (in Scala);

diff -r be9dace0ff58 -r ec75dc58688b src/Pure/Concurrent/volatile.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/volatile.scala	Sat Aug 28 17:20:53 2010 +0200
@@ -0,0 +1,22 @@
+/*  Title:      Pure/Concurrent/volatile.scala
+    Author:     Makarius
+
+Volatile variables.
+*/
+
+package isabelle
+
+
+class Volatile[A](init: A)
+{
+  @volatile private var state: A = init
+  def peek(): A = state
+  def change(f: A => A) { state = f(state) }
+  def change_yield[B](f: A => (B, A)): B =
+  {
+    val (result, new_state) = f(state)
+    state = new_state
+    result
+  }
+}
+
diff -r be9dace0ff58 -r ec75dc58688b src/Pure/build-jars
--- a/src/Pure/build-jars	Sat Aug 28 15:25:32 2010 +0200
+++ b/src/Pure/build-jars	Sat Aug 28 17:20:53 2010 +0200
@@ -24,6 +24,7 @@
 declare -a SOURCES=(
   Concurrent/future.scala
   Concurrent/simple_thread.scala
+  Concurrent/volatile.scala
   General/exn.scala
   General/linear_set.scala
   General/markup.scala