| changeset 63805 | c272680df665 |
| parent 56744 | 0b74d1df4b8e |
| child 64370 | 865b39487b5d |
--- a/src/Pure/PIDE/document_id.scala Mon Sep 05 21:09:50 2016 +0200 +++ b/src/Pure/PIDE/document_id.scala Mon Sep 05 22:09:52 2016 +0200 @@ -20,7 +20,7 @@ val none: Generic = 0 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) + def apply(id: Generic): String = Value.Long.apply(id) + def unapply(s: String): Option[Generic] = Value.Long.unapply(s) }