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 |
}
|