# HG changeset patch
# User wenzelm
# Date 1607633333 -3600
# Node ID 313c281766cd13a5e56b1955cd0386cea89d8756
# Parent  626fcaebd049d5deff39eba8ed0ed0db7578be67
clarified messages;

diff -r 626fcaebd049 -r 313c281766cd src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 10 18:38:26 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 10 21:48:53 2020 +0100
@@ -192,17 +192,20 @@
           else if (is_information(elem)) "Information"
           else if (is_tracing(elem)) "Tracing"
           else "Output"
-        h + Position.here(pos) + ":\n"
+        "\n" + h + Position.here(pos) + ":\n"
       }
       else ""
-    val text2 =
+
+    val body =
       Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
         margin = margin, breakgain = breakgain, metric = metric)
 
-    val text = text1 + text2
-    if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(text)
-    else if (is_error(elem)) Output.error_prefix(text)
-    else text
+    val text2 =
+      if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)
+      else if (is_error(elem)) Output.error_prefix(body)
+      else body
+
+    text1 + text2
   }