eliminated redundant Volatile;
authorwenzelm
Thu Apr 24 10:38:14 2014 +0200 (2014-04-24)
changeset 5669069b31dc7256e
parent 56689 b8b8b4ff8ad5
child 56691 ad5d7461b370
eliminated redundant Volatile;
src/Pure/Concurrent/volatile.scala
src/Pure/PIDE/session.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Concurrent/volatile.scala	Thu Apr 24 10:33:06 2014 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,31 +0,0 @@
     1.4 -/*  Title:      Pure/Concurrent/volatile.scala
     1.5 -    Module:     PIDE
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Volatile variables.
     1.9 -*/
    1.10 -
    1.11 -package isabelle
    1.12 -
    1.13 -
    1.14 -object Volatile
    1.15 -{
    1.16 -  def apply[A](init: A): Volatile[A] = new Volatile(init)
    1.17 -}
    1.18 -
    1.19 -
    1.20 -final class Volatile[A] private(init: A)
    1.21 -{
    1.22 -  @volatile private var state: A = init
    1.23 -  def value: A = state
    1.24 -  def change(f: A => A) { state = f(state) }
    1.25 -  def change_result[B](f: A => (B, A)): B =
    1.26 -  {
    1.27 -    val (result, new_state) = f(state)
    1.28 -    state = new_state
    1.29 -    result
    1.30 -  }
    1.31 -
    1.32 -  override def toString: String = state.toString
    1.33 -}
    1.34 -
     2.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 10:33:06 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 10:38:14 2014 +0200
     2.3 @@ -207,7 +207,7 @@
     2.4  
     2.5    /* global state */
     2.6  
     2.7 -  private val syslog = Volatile(Queue.empty[XML.Elem])
     2.8 +  private val syslog = Synchronized(Queue.empty[XML.Elem])
     2.9    def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
    2.10  
    2.11    @volatile private var _phase: Session.Phase = Session.Inactive
    2.12 @@ -219,7 +219,7 @@
    2.13    def phase = _phase
    2.14    def is_ready: Boolean = phase == Session.Ready
    2.15  
    2.16 -  private val global_state = Volatile(Document.State.init)
    2.17 +  private val global_state = Synchronized(Document.State.init)
    2.18    def current_state(): Document.State = global_state.value
    2.19  
    2.20    def recent_syntax(): Prover.Syntax =
     3.1 --- a/src/Pure/build-jars	Thu Apr 24 10:33:06 2014 +0200
     3.2 +++ b/src/Pure/build-jars	Thu Apr 24 10:38:14 2014 +0200
     3.3 @@ -13,7 +13,6 @@
     3.4    Concurrent/future.scala
     3.5    Concurrent/simple_thread.scala
     3.6    Concurrent/synchronized.scala
     3.7 -  Concurrent/volatile.scala
     3.8    General/antiquote.scala
     3.9    General/bytes.scala
    3.10    General/completion.scala