equal
deleted
inserted
replaced
70 } |
70 } |
71 |
71 |
72 |
72 |
73 /* specific messages */ |
73 /* specific messages */ |
74 |
74 |
75 def is_tracing(msg: XML.Tree): Boolean = |
75 def is_ready(msg: XML.Tree): Boolean = |
|
76 msg match { |
|
77 case XML.Elem(Markup(Markup.STATUS, _), |
|
78 List(XML.Elem(Markup(Markup.READY, _), _))) => true |
|
79 case _ => false |
|
80 } |
|
81 |
|
82 def is_tracing(msg: XML.Tree): Boolean = |
76 msg match { |
83 msg match { |
77 case XML.Elem(Markup(Markup.TRACING, _), _) => true |
84 case XML.Elem(Markup(Markup.TRACING, _), _) => true |
78 case _ => false |
85 case _ => false |
79 } |
86 } |
80 |
87 |