src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jul 12 19:36:46 2011 +0200
@@ -16,12 +16,7 @@
   /* formal identifiers */
 
   type ID = Long
-
-  object ID
-  {
-    def apply(id: ID): String = Markup.Long.apply(id)
-    def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
-  }
+  val ID = Properties.Value.Long
 
   type Version_ID = ID
   type Command_ID = ID