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