--- a/src/Pure/Tools/build.scala Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/Tools/build.scala Wed Apr 01 20:17:23 2020 +0200
@@ -161,8 +161,8 @@
{
val errors =
try {
- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)).
- map(err => Pretty.string_of(Protocol_Message.expose_no_reports(err)))
+ for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text))) yield
+ Pretty.string_of(Protocol_Message.expose_no_reports(err), metric = Symbol.Metric)
}
catch { case ERROR(err) => List(err) }
build_session_errors.fulfill(errors)
@@ -269,7 +269,8 @@
stdout ++= Symbol.encode(XML.content(message))
}
else if (Protocol.is_exported(message)) {
- messages += Symbol.encode(Protocol.message_text(List(message)))
+ messages +=
+ Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))
}
case _ =>
}