| 43660 |      1 | /*  Title:      Pure/Concurrent/counter.scala
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Synchronized counter for unique identifiers < 0.
 | 
|  |      5 | 
 | 
|  |      6 | NB: ML ticks forwards, JVM ticks backwards.
 | 
|  |      7 | */
 | 
|  |      8 | 
 | 
|  |      9 | package isabelle
 | 
|  |     10 | 
 | 
|  |     11 | 
 | 
| 75393 |     12 | object Counter {
 | 
| 43660 |     13 |   type ID = Long
 | 
| 52537 |     14 |   def make(): Counter = new Counter
 | 
| 43660 |     15 | }
 | 
|  |     16 | 
 | 
| 75393 |     17 | final class Counter private {
 | 
| 43660 |     18 |   private var count: Counter.ID = 0
 | 
|  |     19 | 
 | 
|  |     20 |   def apply(): Counter.ID = synchronized {
 | 
| 78243 |     21 |     require(count > Long.MinValue, "counter overflow")
 | 
| 43660 |     22 |     count -= 1
 | 
|  |     23 |     count
 | 
|  |     24 |   }
 | 
| 56685 |     25 | 
 | 
|  |     26 |   override def toString: String = count.toString
 | 
| 43660 |     27 | }
 |