# HG changeset patch
# User wenzelm
# Date 1585758139 -7200
# Node ID 7b0656fa783bd21b08a067024b650c9e816905ce
# Parent  86f064893dac551e252769bc6a23df1b27478dfd
clarified signature;

diff -r 86f064893dac -r 7b0656fa783b src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Wed Apr 01 18:19:46 2020 +0200
+++ b/src/Pure/General/output.scala	Wed Apr 01 18:22:19 2020 +0200
@@ -15,11 +15,11 @@
 
   def writeln_text(msg: String): String = clean_yxml(msg)
 
-  def warning_text(msg: String): String =
-    Library.prefix_lines("### ", clean_yxml(msg))
+  def warning_prefix(s: String): String = Library.prefix_lines("### ", s)
+  def warning_text(msg: String): String = warning_prefix(clean_yxml(msg))
 
-  def error_message_text(msg: String): String =
-    Library.prefix_lines("*** ", clean_yxml(msg))
+  def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
+  def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
 
   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {
diff -r 86f064893dac -r 7b0656fa783b src/Pure/PIDE/protocol.scala
--- 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
   }