--- a/src/Pure/PIDE/document_id.scala Mon Aug 14 14:41:22 2017 +0200
+++ b/src/Pure/PIDE/document_id.scala Mon Aug 14 15:30:26 2017 +0200
@@ -22,4 +22,3 @@
def apply(id: Generic): String = Value.Long.apply(id)
def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
}
-