| author | blanchet | 
| Wed, 18 Apr 2012 22:39:35 +0200 | |
| changeset 47558 | 55b42f9af99d | 
| parent 46712 | 8650d9a95736 | 
| child 52537 | 4b5941730bd8 | 
| 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  | 
|
| 45243 | 16  | 
def apply(): 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  | 
}  | 
|
28  | 
}  | 
|
29  |