--- a/src/Pure/PIDE/isar_document.scala Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Thu Aug 11 18:01:28 2011 +0200
@@ -144,7 +144,12 @@
{
val arg1 =
{ import XML.Encode._
- list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
+ def encode: T[List[Document.Edit_Command_ID]] =
+ list(pair(string,
+ variant(List(
+ { case Document.Node.Remove() => (Nil, Nil) },
+ { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }))))
+ encode(edits) }
val arg2 =
{ import XML.Encode._