--- a/src/Pure/PIDE/protocol.scala Mon Nov 25 12:41:52 2019 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Nov 25 13:28:31 2019 +0100
@@ -150,6 +150,14 @@
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 =
+ {
+ 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)
+ else text
+ }
+
/* breakpoints */