diff -r a21a29de5f57 -r 03afc8252225 src/Pure/PIDE/protocol.scala
--- 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 */