eliminated redundant Volatile;

--- a/src/Pure/Concurrent/volatile.scala	Thu Apr 24 10:33:06 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/*  Title:      Pure/Concurrent/volatile.scala
-    Module:     PIDE
-    Author:     Makarius
-
-Volatile variables.
-*/
-
-package isabelle
-
-
-object Volatile
-{
-  def apply[A](init: A): Volatile[A] = new Volatile(init)
-}
-
-
-final class Volatile[A] private(init: A)
-{
-  @volatile private var state: A = init
-  def value: A = state
-  def change(f: A => A) { state = f(state) }
-  def change_result[B](f: A => (B, A)): B =
-  {
-    val (result, new_state) = f(state)
-    state = new_state
-    result
-  }
-
-  override def toString: String = state.toString
-}
-

--- a/src/Pure/PIDE/session.scala	Thu Apr 24 10:33:06 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 24 10:38:14 2014 +0200
@@ -207,7 +207,7 @@
 
   /* global state */
 
-  private val syslog = Volatile(Queue.empty[XML.Elem])
+  private val syslog = Synchronized(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
@@ -219,7 +219,7 @@
   def phase = _phase
   def is_ready: Boolean = phase == Session.Ready
 
-  private val global_state = Volatile(Document.State.init)
+  private val global_state = Synchronized(Document.State.init)
   def current_state(): Document.State = global_state.value
 
   def recent_syntax(): Prover.Syntax =

--- a/src/Pure/build-jars	Thu Apr 24 10:33:06 2014 +0200
+++ b/src/Pure/build-jars	Thu Apr 24 10:38:14 2014 +0200
@@ -13,7 +13,6 @@
   Concurrent/future.scala
   Concurrent/simple_thread.scala
   Concurrent/synchronized.scala
-  Concurrent/volatile.scala
   General/antiquote.scala
   General/bytes.scala
   General/completion.scala