--- a/src/Pure/PIDE/document_id.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/document_id.scala Fri Jul 05 16:01:45 2013 +0200
@@ -11,14 +11,15 @@
object Document_ID
{
- type ID = Long
- val ID = Properties.Value.Long
+ type Generic = Long
+ type Version = Generic
+ type Command = Generic
+ type Exec = Generic
- type Version = ID
- type Command = ID
- type Exec = ID
+ val none: Generic = 0
+ val make = Counter()
- val none: ID = 0
- val make = Counter()
+ def apply(id: Generic): String = Properties.Value.Long.apply(id)
+ def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
}