--- 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
}
}