# HG changeset patch
# User wenzelm
# Date 1319318904 -7200
# Node ID 3b7b64b194ee8cc3d1e0d0def27afe5b29075ab3
# Parent  d7f5338f03356bf379693fbe2d12dca611189a35
class Volatile as abstract datatype;

diff -r d7f5338f0335 -r 3b7b64b194ee src/Pure/Concurrent/volatile.scala
--- a/src/Pure/Concurrent/volatile.scala	Sat Oct 22 20:18:01 2011 +0200
+++ b/src/Pure/Concurrent/volatile.scala	Sat Oct 22 23:28:24 2011 +0200
@@ -7,7 +7,13 @@
 package isabelle
 
 
-class Volatile[A](init: A)
+object Volatile
+{
+  def apply[A](init: A): Volatile[A] = new Volatile(init)
+}
+
+
+class Volatile[A] private(init: A)
 {
   @volatile private var state: A = init
   def apply(): A = state
diff -r d7f5338f0335 -r 3b7b64b194ee src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Oct 22 20:18:01 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Oct 22 23:28:24 2011 +0200
@@ -104,7 +104,7 @@
   def phase = _phase
   def is_ready: Boolean = phase == Session.Ready
 
-  private val global_state = new Volatile(Document.State.init)
+  private val global_state = Volatile(Document.State.init)
   def current_state(): Document.State = global_state()
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,