author | wenzelm |
Sun, 09 Oct 2011 16:47:58 +0200 | |
changeset 45107 | 76fef3e57004 |
parent 43660 | bfc0bb115fa1 |
child 45243 | 27466646a7a3 |
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 |
|
15 |
} |
|
16 |
||
17 |
class Counter |
|
18 |
{ |
|
19 |
private var count: Counter.ID = 0 |
|
20 |
||
21 |
def apply(): Counter.ID = synchronized { |
|
22 |
require(count > java.lang.Long.MIN_VALUE) |
|
23 |
count -= 1 |
|
24 |
count |
|
25 |
} |
|
26 |
} |
|
27 |