# HG changeset patch
# User wenzelm
# Date 1590484630 -7200
# Node ID ab21876c30c1d5b78e3b8c8a0e5bbf652e49a3f4
# Parent  a27747c857007e5f14d6f57127d386b1f6b32ae3
tuned;

diff -r a27747c85700 -r ab21876c30c1 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Mon May 25 22:37:22 2020 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 26 11:17:10 2020 +0200
@@ -250,7 +250,7 @@
         val Threads_Option = """threads\s*=\s*(\d+)""".r
 
         val sql = profile.select(options, columns, only_sessions)
-        if (verbose) progress.echo(sql)
+        progress.echo_if(verbose, sql)
 
         db.using_statement(sql)(stmt =>
         {
diff -r a27747c85700 -r ab21876c30c1 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon May 25 22:37:22 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 26 11:17:10 2020 +0200
@@ -718,7 +718,7 @@
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
-                  if (verbose) progress.echo("Skipping " + session_name + " ...")
+                  progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
diff -r a27747c85700 -r ab21876c30c1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon May 25 22:37:22 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Tue May 26 11:17:10 2020 +0200
@@ -483,7 +483,7 @@
 
       val start_date = Date.now()
 
-      if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date))
+      progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
 
       progress.interrupt_handler {
         dump(options, logic,
@@ -505,7 +505,7 @@
       val end_date = Date.now()
       val timing = end_date.time - start_date.time
 
-      if (verbose) progress.echo("\nFinished at " + Build_Log.print_date(end_date))
+      progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
       progress.echo(timing.message_hms + " elapsed time")
     })
 }