# HG changeset patch
# User wenzelm
# Date 1607616889 -3600
# Node ID 2206502637e41ce81df113ed276b19cd36f79ea2
# Parent  0ad513706a27a59f19ae9d0e2807d301a7771887
clarified types;

diff -r 0ad513706a27 -r 2206502637e4 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 10 17:09:06 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 10 17:14:49 2020 +0100
@@ -116,12 +116,6 @@
 
   /* 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
@@ -183,17 +177,17 @@
   def is_exported(msg: XML.Tree): Boolean =
     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
 
-  def message_text(body: XML.Body,
+  def message_text(elem: XML.Elem,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
     metric: Pretty.Metric = Pretty.Default_Metric): String =
   {
     val text =
-      Pretty.string_of(Protocol_Message.expose_no_reports(body),
+      Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
         margin = margin, breakgain = breakgain, metric = metric)
 
-    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)
+    if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(text)
+    else if (is_error(elem)) Output.error_prefix(text)
     else text
   }
 
diff -r 0ad513706a27 -r 2206502637e4 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 17:09:06 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 17:14:49 2020 +0100
@@ -124,9 +124,9 @@
                 val messages = rendering.text_messages(Text.Range.full)
                 if (messages.nonEmpty) {
                   progress.echo(thy_heading)
-                  for (Text.Info(_, t) <- messages) {
+                  for (Text.Info(_, elem) <- messages) {
                     progress.echo(
-                      Protocol.message_text(List(t), margin = margin, breakgain = breakgain,
+                      Protocol.message_text(elem, margin = margin, breakgain = breakgain,
                         metric = metric))
                   }
                 }
@@ -470,7 +470,7 @@
         val more_output =
           Library.trim_line(stdout.toString) ::
             messages.toList.map(message =>
-              Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
+              Symbol.encode(Protocol.message_text(message, metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::