equal
deleted
inserted
replaced
590 }).exists(_.info) |
590 }).exists(_.info) |
591 |
591 |
592 message_colors.get(pri).map((_, is_separator)) |
592 message_colors.get(pri).map((_, is_separator)) |
593 } |
593 } |
594 |
594 |
595 def output_messages(st: Command.State): List[XML.Tree] = |
595 def output_messages(results: Command.Results): List[XML.Tree] = |
596 st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList |
596 results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList |
597 |
597 |
598 |
598 |
599 /* text background */ |
599 /* text background */ |
600 |
600 |
601 def background(range: Text.Range): List[Text.Info[Color]] = |
601 def background(range: Text.Range): List[Text.Info[Color]] = |