equal
deleted
inserted
replaced
76 values -- background_colors -- foreground_colors -- message_underline_colors -- |
76 values -- background_colors -- foreground_colors -- message_underline_colors -- |
77 message_background_colors |
77 message_background_colors |
78 } |
78 } |
79 |
79 |
80 |
80 |
81 /* message priorities */ |
81 /* output messages */ |
82 |
82 |
83 val state_pri = 1 |
83 val state_pri = 1 |
84 val writeln_pri = 2 |
84 val writeln_pri = 2 |
85 val information_pri = 3 |
85 val information_pri = 3 |
86 val tracing_pri = 4 |
86 val tracing_pri = 4 |
117 information_pri -> Color.information_message, |
117 information_pri -> Color.information_message, |
118 tracing_pri -> Color.tracing_message, |
118 tracing_pri -> Color.tracing_message, |
119 warning_pri -> Color.warning_message, |
119 warning_pri -> Color.warning_message, |
120 legacy_pri -> Color.legacy_message, |
120 legacy_pri -> Color.legacy_message, |
121 error_pri -> Color.error_message) |
121 error_pri -> Color.error_message) |
|
122 |
|
123 def output_messages(results: Command.Results): List[XML.Tree] = |
|
124 { |
|
125 val (states, other) = |
|
126 results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList |
|
127 .partition(Protocol.is_state(_)) |
|
128 states ::: other |
|
129 } |
122 |
130 |
123 |
131 |
124 /* text color */ |
132 /* text color */ |
125 |
133 |
126 val text_color = Map( |
134 val text_color = Map( |