| 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 | 
 | 
|  |     12 | object Counter
 | 
|  |     13 | {
 | 
|  |     14 |   type ID = Long
 | 
| 52537 |     15 |   def make(): Counter = new Counter
 | 
| 43660 |     16 | }
 | 
|  |     17 | 
 | 
| 46712 |     18 | final class Counter private
 | 
| 43660 |     19 | {
 | 
|  |     20 |   private var count: Counter.ID = 0
 | 
|  |     21 | 
 | 
|  |     22 |   def apply(): Counter.ID = synchronized {
 | 
|  |     23 |     require(count > java.lang.Long.MIN_VALUE)
 | 
|  |     24 |     count -= 1
 | 
|  |     25 |     count
 | 
|  |     26 |   }
 | 
| 56685 |     27 | 
 | 
|  |     28 |   override def toString: String = count.toString
 | 
| 43660 |     29 | }
 |