# HG changeset patch
# User wenzelm
# Date 1607618506 -3600
# Node ID 847c6fb05a215dc97fd9bed2e99515079486dbc5
# Parent  2206502637e41ce81df113ed276b19cd36f79ea2
clarified messages;

diff -r 2206502637e4 -r 847c6fb05a21 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 10 17:14:49 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 10 17:41:46 2020 +0100
@@ -178,14 +178,28 @@
     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
 
   def message_text(elem: XML.Elem,
+    heading: Boolean = false,
+    pos: Position.T = Position.none,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
     metric: Pretty.Metric = Pretty.Default_Metric): String =
   {
-    val text =
+    val text1 =
+      if (heading) {
+        val h =
+          if (is_warning(elem) || is_legacy(elem)) "Warning"
+          else if (is_error(elem)) "Error"
+          else if (is_information(elem)) "Information"
+          else if (is_tracing(elem)) "Tracing"
+          else "Output"
+        h + Position.here(pos) + ":\n"
+      }
+      else ""
+    val text2 =
       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
diff -r 2206502637e4 -r 847c6fb05a21 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 17:14:49 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 17:41:46 2020 +0100
@@ -123,11 +123,14 @@
                 val rendering = new Rendering(snapshot, options, session)
                 val messages = rendering.text_messages(Text.Range.full)
                 if (messages.nonEmpty) {
+                  val line_document = Line.Document(command.source)
                   progress.echo(thy_heading)
-                  for (Text.Info(_, elem) <- messages) {
+                  for (Text.Info(range, elem) <- messages) {
+                    val line = line_document.position(range.start).line1
+                    val pos = Position.Line_File(line, command.node_name.node)
                     progress.echo(
-                      Protocol.message_text(elem, margin = margin, breakgain = breakgain,
-                        metric = metric))
+                      Protocol.message_text(elem, heading = true, pos = pos,
+                        margin = margin, breakgain = breakgain, metric = metric))
                   }
                 }
             }