equal
deleted
inserted
replaced
167 !(is_result(msg) || is_tracing(msg) || is_state(msg)) |
167 !(is_result(msg) || is_tracing(msg) || is_state(msg)) |
168 |
168 |
169 def is_exported(msg: XML.Tree): Boolean = |
169 def is_exported(msg: XML.Tree): Boolean = |
170 is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) |
170 is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) |
171 |
171 |
172 def message_text(body: XML.Body, margin: Double = Pretty.default_margin): String = |
172 def message_text(body: XML.Body, |
173 { |
173 margin: Double = Pretty.default_margin, |
174 val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin) |
174 breakgain: Double = Pretty.default_breakgain, |
|
175 metric: Pretty.Metric = Pretty.Default_Metric): String = |
|
176 { |
|
177 val text = |
|
178 Pretty.string_of(Protocol_Message.expose_no_reports(body), |
|
179 margin = margin, breakgain = breakgain, metric = metric) |
|
180 |
175 if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) |
181 if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) |
176 else if (is_message(is_error, body)) Output.error_prefix(text) |
182 else if (is_message(is_error, body)) Output.error_prefix(text) |
177 else text |
183 else text |
178 } |
184 } |
179 |
185 |