diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Mon Aug 22 21:09:26 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Mon Aug 22 21:42:02 2011 +0200 @@ -152,7 +152,8 @@ { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) }, - { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) })))) + { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, + { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) })))) YXML.string_of_body(encode(edits)) } input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)