diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -16,15 +16,18 @@
   /* 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)
+  }
+
   type Version_ID = ID
   type Command_ID = ID
   type Exec_ID = ID
 
   val NO_ID: ID = 0
 
-  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
-  def print_id(id: ID): String = id.toString
-
 
 
   /** named document nodes **/