| changeset 64370 | 865b39487b5d |
| parent 56685 | 535d59d4ed12 |
| child 64443 | 857acb970dfa |
| 64369:6a9816764b37 | 64370:865b39487b5d |
|---|---|
1 /* Title: Pure/Concurrent/counter.scala |
1 /* Title: Pure/Concurrent/counter.scala |
2 Module: PIDE |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Synchronized counter for unique identifiers < 0. |
4 Synchronized counter for unique identifiers < 0. |
6 |
5 |
7 NB: ML ticks forwards, JVM ticks backwards. |
6 NB: ML ticks forwards, JVM ticks backwards. |