tuned: trim message before formatting;

--- a/src/Pure/Build/build_job.scala	Thu Sep 12 14:38:19 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Thu Sep 12 14:42:04 2024 +0200
@@ -233,8 +233,7 @@
                     }
                     val errors =
                       for (err <- errs) yield {
-                        val prt = Protocol_Message.expose_no_reports(err)
-                        Pretty.string_of(prt, metric = Symbol.Metric)
+                        Pretty.string_of(err, metric = Symbol.Metric, pure = true)
                       }
                     (rc, errors)
                   }

--- a/src/Pure/PIDE/protocol.scala	Thu Sep 12 14:38:19 2024 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Sep 12 14:42:04 2024 +0200
@@ -189,8 +189,8 @@
     val text1 = if (heading) "\n" + message_heading(elem, pos) + ":\n" else ""
 
     val body =
-      Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
-        margin = margin, breakgain = breakgain, metric = metric)
+      Pretty.string_of(List(elem), margin = margin, breakgain = breakgain,
+        metric = metric, pure = true)
 
     val text2 =
       if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)

--- a/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 14:38:19 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 14:42:04 2024 +0200
@@ -43,9 +43,6 @@
   def clean_reports(body: XML.Body): XML.Body =
     XML.filter_elements(body, remove = any_report_elements)
 
-  def expose_no_reports(body: XML.Body): XML.Body =
-    XML.filter_elements(body, expose = no_report_elements)
-
   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
     body flatMap {
       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>