src/Pure/Concurrent/volatile.scala
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 46712 8650d9a95736
child 56685 535d59d4ed12
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
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
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
38840
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     4
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     5
Volatile variables.
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     6
*/
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     7
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     8
package isabelle
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
     9
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    10
45248
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    11
object Volatile
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    12
{
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    13
  def apply[A](init: A): Volatile[A] = new Volatile(init)
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    14
}
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    15
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 43719
diff changeset
    16
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46687
diff changeset
    17
final class Volatile[A] private(init: A)
38840
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    18
{
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    19
  @volatile private var state: A = init
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 38840
diff changeset
    20
  def apply(): A = state
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 45673
diff changeset
    21
  def >> (f: A => A) { state = f(state) }
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 45673
diff changeset
    22
  def >>>[B] (f: A => (B, A)): B =
38840
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    23
  {
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    24
    val (result, new_state) = f(state)
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    25
    state = new_state
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    26
    result
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    27
  }
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    28
}
ec75dc58688b volatile variables (in Scala);
wenzelm
parents:
diff changeset
    29