diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 03 21:15:35 2011 +0200
@@ -26,6 +26,20 @@
       }
   }
 
+  object Removed
+  {
+    def unapply(text: String): Option[List[Document.Version_ID]] =
+      try {
+        import XML.Decode._
+        Some(list(long)(YXML.parse_body(text)))
+      }
+      catch {
+        case ERROR(_) => None
+        case _: XML.XML_Atom => None
+        case _: XML.XML_Body => None
+      }
+  }
+
 
   /* toplevel transactions */