equal
deleted
inserted
replaced
95 error_pri -> Color.error_message) |
95 error_pri -> Color.error_message) |
96 |
96 |
97 def output_messages(results: Command.Results): List[XML.Tree] = |
97 def output_messages(results: Command.Results): List[XML.Tree] = |
98 { |
98 { |
99 val (states, other) = |
99 val (states, other) = |
100 results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList |
100 results.iterator.map(_._2).filterNot(Protocol.is_result).toList |
101 .partition(Protocol.is_state(_)) |
101 .partition(Protocol.is_state) |
102 states ::: other |
102 states ::: other |
103 } |
103 } |
104 |
104 |
105 |
105 |
106 /* text color */ |
106 /* text color */ |