src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Jul 09 13:17:22 2013 +0200
@@ -11,9 +11,9 @@
 {
   /* document editing */
 
-  object Assign
+  object Assign_Update
   {
-    def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
+    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
       try {
         import XML.Decode._
         val body = YXML.parse_body(text)