src/Pure/Concurrent/volatile.scala

discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

/*  Title:      Pure/Concurrent/volatile.scala
    Author:     Makarius

Volatile variables.
*/

package isabelle


class Volatile[A](init: A)
{
  @volatile private var state: A = init
  def apply(): A = state
  def change(f: A => A) { state = f(state) }
  def change_yield[B](f: A => (B, A)): B =
  {
    val (result, new_state) = f(state)
    state = new_state
    result
  }
}