prefer explicit progress channel;
authorwenzelm
Sun May 14 17:19:46 2017 +0200 (2017-05-14)
changeset 658313b197547c1d4
parent 65830 064925cb656f
child 65832 2fb85623c386
prefer explicit progress channel;
src/Pure/System/numa.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/System/numa.scala	Sun May 14 17:19:22 2017 +0200
     1.2 +++ b/src/Pure/System/numa.scala	Sun May 14 17:19:46 2017 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5    /* shuffling of CPU nodes */
     1.6  
     1.7 -  def enabled_warning(enabled: Boolean): Boolean =
     1.8 +  def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
     1.9    {
    1.10      def warning =
    1.11        if (nodes().length < 2) Some("no NUMA nodes available")
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14      enabled &&
    1.15        (warning match {
    1.16 -        case Some(s) => Output.warning("Shuffling of CPU nodes is disabled: " + s); false
    1.17 +        case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
    1.18          case _ => true
    1.19        })
    1.20    }
     2.1 --- a/src/Pure/Tools/build.scala	Sun May 14 17:19:22 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sun May 14 17:19:46 2017 +0200
     2.3 @@ -34,7 +34,8 @@
     2.4  
     2.5    private object Queue
     2.6    {
     2.7 -    def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
     2.8 +    def load_timings(progress: Progress, store: Sessions.Store, name: String)
     2.9 +      : (List[Properties.T], Double) =
    2.10      {
    2.11        val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    2.12  
    2.13 @@ -43,7 +44,7 @@
    2.14          case Some(database) =>
    2.15            def ignore_error(msg: String) =
    2.16            {
    2.17 -            Output.warning("Ignoring bad database: " +
    2.18 +            progress.echo_warning("Ignoring bad database: " +
    2.19                database.expand + (if (msg == "") "" else "\n" + msg))
    2.20              no_timings
    2.21            }
    2.22 @@ -63,12 +64,12 @@
    2.23        }
    2.24      }
    2.25  
    2.26 -    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
    2.27 +    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
    2.28      {
    2.29        val graph = sessions.build_graph
    2.30        val names = graph.keys
    2.31  
    2.32 -      val timings = names.map(name => (name, load_timings(store, name)))
    2.33 +      val timings = names.map(name => (name, load_timings(progress, store, name)))
    2.34        val command_timings =
    2.35          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    2.36        val session_timing =
    2.37 @@ -380,7 +381,7 @@
    2.38      /* main build process */
    2.39  
    2.40      val store = Sessions.store(system_mode)
    2.41 -    val queue = Queue(selected_sessions, store)
    2.42 +    val queue = Queue(progress, selected_sessions, store)
    2.43  
    2.44      store.prepare_output()
    2.45  
    2.46 @@ -683,7 +684,7 @@
    2.47            clean_build = clean_build,
    2.48            dirs = dirs,
    2.49            select_dirs = select_dirs,
    2.50 -          numa_shuffling = NUMA.enabled_warning(numa_shuffling),
    2.51 +          numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
    2.52            max_jobs = max_jobs,
    2.53            list_files = list_files,
    2.54            check_keywords = check_keywords,