| changeset 52537 | 4b5941730bd8 |
| parent 52531 | 21f8e0e151f5 |
| child 56744 | 0b74d1df4b8e |
--- a/src/Pure/PIDE/document_id.scala Fri Jul 05 22:58:24 2013 +0200 +++ b/src/Pure/PIDE/document_id.scala Fri Jul 05 23:10:18 2013 +0200 @@ -17,7 +17,7 @@ type Exec = Generic val none: Generic = 0 - val make = Counter() + val make = Counter.make() def apply(id: Generic): String = Properties.Value.Long.apply(id) def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)