--- 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
})
}
--- 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,