equal
deleted
inserted
replaced
434 }).exists(_.info) |
434 }).exists(_.info) |
435 (message_color, is_separator) |
435 (message_color, is_separator) |
436 }) |
436 }) |
437 } |
437 } |
438 |
438 |
439 def output_messages(results: Command.Results): List[XML.Tree] = |
|
440 { |
|
441 val (states, other) = |
|
442 results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList |
|
443 .partition(Protocol.is_state(_)) |
|
444 states ::: other |
|
445 } |
|
446 |
|
447 |
439 |
448 /* text color */ |
440 /* text color */ |
449 |
441 |
450 def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] = |
442 def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] = |
451 { |
443 { |