author | wenzelm |
Wed, 20 Oct 2021 18:13:17 +0200 | |
changeset 74561 | 8e6c973003c8 |
parent 73120 | c3589f2dff31 |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
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 { |
|
73120
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents:
64443
diff
changeset
|
23 |
require(count > java.lang.Long.MIN_VALUE, "counter overflow") |
43660 | 24 |
count -= 1 |
25 |
count |
|
26 |
} |
|
56685 | 27 |
|
28 |
override def toString: String = count.toString |
|
43660 | 29 |
} |