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;

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

Synchronized counter for unique identifiers < 0.

NB: ML ticks forwards, JVM ticks backwards.
*/

package isabelle


object Counter
{
  type ID = Long
}

class Counter
{
  private var count: Counter.ID = 0

  def apply(): Counter.ID = synchronized {
    require(count > java.lang.Long.MIN_VALUE)
    count -= 1
    count
  }
}