--- a/src/Pure/Tools/build.scala Sun May 14 17:00:57 2017 +0200
+++ b/src/Pure/Tools/build.scala Sun May 14 17:01:05 2017 +0200
@@ -551,7 +551,7 @@
val results0 =
if (deps.is_empty) {
- progress.echo(Output.warning_text("Nothing to build"))
+ progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
--- a/src/Pure/Tools/check_keywords.scala Sun May 14 17:00:57 2017 +0200
+++ b/src/Pure/Tools/check_keywords.scala Sun May 14 17:01:05 2017 +0200
@@ -46,9 +46,8 @@
}, parallel_args).flatten
for ((tok, pos) <- bad) {
- progress.echo(Output.warning_text(
- "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
- Position.here(pos)))
+ progress.echo_warning(
+ "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
}
}
}