# HG changeset patch
# User wenzelm
# Date 1494774065 -7200
# Node ID 3bba3856b56c7563b546d601bdb66c2bd07b80dc
# Parent  0b8a6a62114fe9a1e571321662d10a564a609d89
tuned;

diff -r 0b8a6a62114f -r 3bba3856b56c src/Pure/Tools/build.scala
--- 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)
diff -r 0b8a6a62114f -r 3bba3856b56c src/Pure/Tools/check_keywords.scala
--- 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))
     }
   }
 }