equal
deleted
inserted
replaced
16 def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] = |
16 def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] = |
17 msg match { |
17 msg match { |
18 case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) => |
18 case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) => |
19 try { |
19 try { |
20 import XML.Decode._ |
20 import XML.Decode._ |
21 val a = pair(list(pair(long, long)), list(pair(string, option(long))))(body) |
21 val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body) |
22 Some(id, a) |
22 Some(id, a) |
23 } |
23 } |
24 catch { |
24 catch { |
25 case _: XML.XML_Atom => None |
25 case _: XML.XML_Atom => None |
26 case _: XML.XML_Body => None |
26 case _: XML.XML_Body => None |