src/Pure/Concurrent/volatile.scala
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 38840 ec75dc58688b
child 43719 ba1b2c918c32
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38840
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/volatile.scala
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     3
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     4
Volatile variables.
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     5
*/
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     6
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     7
package isabelle
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     8
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     9
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    10
class Volatile[A](init: A)
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    11
{
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    12
  @volatile private var state: A = init
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    13
  def peek(): A = state
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    14
  def change(f: A => A) { state = f(state) }
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    15
  def change_yield[B](f: A => (B, A)): B =
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    16
  {
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    17
    val (result, new_state) = f(state)
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    18
    state = new_state
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    19
    result
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    20
  }
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    21
}
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    22