src/Pure/Concurrent/counter.scala
author wenzelm
Mon, 06 Feb 2023 11:05:35 +0100
changeset 77205 a197d583bf9f
parent 75393 87ebf5a50283
child 78243 0e221a8128e4
permissions -rw-r--r--
proper symbolic dependencies, e.g. for Demo_FoilTeX;

/*  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
  def make(): Counter = new Counter
}

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

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

  override def toString: String = count.toString
}