--- a/src/Pure/PIDE/protocol.scala Wed Apr 01 18:19:46 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Apr 01 18:22:19 2020 +0200
@@ -102,6 +102,12 @@
/* result messages */
+ def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean =
+ body match {
+ case List(elem: XML.Elem) => pred(elem)
+ case _ => false
+ }
+
def is_result(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -163,11 +169,11 @@
def is_exported(msg: XML.Tree): Boolean =
is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
- def message_text(msg: XML.Tree): String =
+ def message_text(body: XML.Body, margin: Double = Pretty.default_margin): String =
{
- val text = Pretty.string_of(List(msg))
- if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text)
- else if (is_error(msg)) Library.prefix_lines("*** ", text)
+ val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin)
+ if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text)
+ else if (is_message(is_error, body)) Output.error_prefix(text)
else text
}