author | blanchet |
Wed, 01 Apr 2015 19:17:41 +0200 | |
changeset 59873 | 2d929c178283 |
parent 56685 | 535d59d4ed12 |
child 64370 | 865b39487b5d |
permissions | -rw-r--r-- |
43660 | 1 |
/* Title: Pure/Concurrent/counter.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
43660 | 3 |
Author: Makarius |
4 |
||
5 |
Synchronized counter for unique identifiers < 0. |
|
6 |
||
7 |
NB: ML ticks forwards, JVM ticks backwards. |
|
8 |
*/ |
|
9 |
||
10 |
package isabelle |
|
11 |
||
12 |
||
13 |
object Counter |
|
14 |
{ |
|
15 |
type ID = Long |
|
52537 | 16 |
def make(): Counter = new Counter |
43660 | 17 |
} |
18 |
||
46712 | 19 |
final class Counter private |
43660 | 20 |
{ |
21 |
private var count: Counter.ID = 0 |
|
22 |
||
23 |
def apply(): Counter.ID = synchronized { |
|
24 |
require(count > java.lang.Long.MIN_VALUE) |
|
25 |
count -= 1 |
|
26 |
count |
|
27 |
} |
|
56685 | 28 |
|
29 |
override def toString: String = count.toString |
|
43660 | 30 |
} |
31 |