diff -r 709e1d671483 -r e8a87398f35d src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 25 16:44:06 2011 +0200
@@ -11,24 +11,20 @@
 {
   /* document editing */
 
-  object Assign {
-    def unapply(msg: XML.Tree)
-        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+  object Assign
+  {
+    def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
       msg match {
-        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
-          val id_edits = edits.map(Edit.unapply)
-          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
-          else None
-        case _ => None
-      }
-  }
-
-  object Edit {
-    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
-      msg match {
-        case XML.Elem(
-          Markup(Markup.EDIT,
-            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
+          try {
+            import XML.Decode._
+            val a = pair(list(pair(long, long)), list(pair(string, option(long))))(body)
+            Some(id, a)
+          }
+          catch {
+            case _: XML.XML_Atom => None
+            case _: XML.XML_Body => None
+          }
         case _ => None
       }
   }