equal
deleted
inserted
replaced
12 /* reports */ |
12 /* reports */ |
13 |
13 |
14 object Assign { |
14 object Assign { |
15 def unapply(msg: XML.Tree): Option[List[XML.Tree]] = |
15 def unapply(msg: XML.Tree): Option[List[XML.Tree]] = |
16 msg match { |
16 msg match { |
17 case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits) |
17 case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits) |
18 case _ => None |
18 case _ => None |
19 } |
19 } |
20 } |
20 } |
21 |
21 |
22 object Edit { |
22 object Edit { |
23 def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] = |
23 def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] = |
24 msg match { |
24 msg match { |
25 case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) => |
25 case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) => |
26 Some(cmd_id, state_id) |
26 Some(cmd_id, state_id) |
27 case _ => None |
27 case _ => None |
28 } |
28 } |
29 } |
29 } |
30 } |
30 } |