class Volatile as abstract datatype;

--- 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

--- 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,