tuned;
authorwenzelm
Sun May 14 17:01:05 2017 +0200 (2017-05-14)
changeset 658273bba3856b56c
parent 65826 0b8a6a62114f
child 65828 02dd430d80c5
tuned;
src/Pure/Tools/build.scala
src/Pure/Tools/check_keywords.scala
     1.1 --- a/src/Pure/Tools/build.scala	Sun May 14 17:00:57 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sun May 14 17:01:05 2017 +0200
     1.3 @@ -551,7 +551,7 @@
     1.4  
     1.5      val results0 =
     1.6        if (deps.is_empty) {
     1.7 -        progress.echo(Output.warning_text("Nothing to build"))
     1.8 +        progress.echo_warning("Nothing to build")
     1.9          Map.empty[String, Result]
    1.10        }
    1.11        else loop(queue, Map.empty, Map.empty)
     2.1 --- a/src/Pure/Tools/check_keywords.scala	Sun May 14 17:00:57 2017 +0200
     2.2 +++ b/src/Pure/Tools/check_keywords.scala	Sun May 14 17:01:05 2017 +0200
     2.3 @@ -46,9 +46,8 @@
     2.4        }, parallel_args).flatten
     2.5  
     2.6      for ((tok, pos) <- bad) {
     2.7 -      progress.echo(Output.warning_text(
     2.8 -        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
     2.9 -          Position.here(pos)))
    2.10 +      progress.echo_warning(
    2.11 +        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
    2.12      }
    2.13    }
    2.14  }