src/Pure/Concurrent/counter.scala
author wenzelm
Sun, 09 Oct 2011 16:47:58 +0200
changeset 45107 76fef3e57004
parent 43660 bfc0bb115fa1
child 45243 27466646a7a3
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43660
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/counter.scala
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     3
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     4
Synchronized counter for unique identifiers < 0.
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     5
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     6
NB: ML ticks forwards, JVM ticks backwards.
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     7
*/
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     8
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
     9
package isabelle
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    10
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    11
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    12
object Counter
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    13
{
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    14
  type ID = Long
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    15
}
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    16
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    17
class Counter
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    18
{
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    19
  private var count: Counter.ID = 0
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    20
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    21
  def apply(): Counter.ID = synchronized {
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    22
    require(count > java.lang.Long.MIN_VALUE)
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    23
    count -= 1
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    24
    count
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    25
  }
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    26
}
bfc0bb115fa1 explicit class Counter;
wenzelm
parents:
diff changeset
    27