--- 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
--- 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))
}
}
}