# HG changeset patch
# User wenzelm
# Date 1494775186 -7200
# Node ID 3b197547c1d489dda3c4ef6457ae35c006b429b3
# Parent  064925cb656fd7dd41151683eb25bbf36124afa3
prefer explicit progress channel;

diff -r 064925cb656f -r 3b197547c1d4 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Sun May 14 17:19:22 2017 +0200
+++ b/src/Pure/System/numa.scala	Sun May 14 17:19:46 2017 +0200
@@ -42,7 +42,7 @@
 
   /* shuffling of CPU nodes */
 
-  def enabled_warning(enabled: Boolean): Boolean =
+  def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
   {
     def warning =
       if (nodes().length < 2) Some("no NUMA nodes available")
@@ -51,7 +51,7 @@
 
     enabled &&
       (warning match {
-        case Some(s) => Output.warning("Shuffling of CPU nodes is disabled: " + s); false
+        case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
         case _ => true
       })
   }
diff -r 064925cb656f -r 3b197547c1d4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 14 17:19:22 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 14 17:19:46 2017 +0200
@@ -34,7 +34,8 @@
 
   private object Queue
   {
-    def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
+    def load_timings(progress: Progress, store: Sessions.Store, name: String)
+      : (List[Properties.T], Double) =
     {
       val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
 
@@ -43,7 +44,7 @@
         case Some(database) =>
           def ignore_error(msg: String) =
           {
-            Output.warning("Ignoring bad database: " +
+            progress.echo_warning("Ignoring bad database: " +
               database.expand + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
@@ -63,12 +64,12 @@
       }
     }
 
-    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
+    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
     {
       val graph = sessions.build_graph
       val names = graph.keys
 
-      val timings = names.map(name => (name, load_timings(store, name)))
+      val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =
@@ -380,7 +381,7 @@
     /* main build process */
 
     val store = Sessions.store(system_mode)
-    val queue = Queue(selected_sessions, store)
+    val queue = Queue(progress, selected_sessions, store)
 
     store.prepare_output()
 
@@ -683,7 +684,7 @@
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
-          numa_shuffling = NUMA.enabled_warning(numa_shuffling),
+          numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,