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