src/Pure/Tools/build.scala
changeset 65831 3b197547c1d4
parent 65828 02dd430d80c5
child 65832 2fb85623c386
     1.1 --- a/src/Pure/Tools/build.scala	Sun May 14 17:19:22 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sun May 14 17:19:46 2017 +0200
     1.3 @@ -34,7 +34,8 @@
     1.4  
     1.5    private object Queue
     1.6    {
     1.7 -    def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
     1.8 +    def load_timings(progress: Progress, store: Sessions.Store, name: String)
     1.9 +      : (List[Properties.T], Double) =
    1.10      {
    1.11        val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    1.12  
    1.13 @@ -43,7 +44,7 @@
    1.14          case Some(database) =>
    1.15            def ignore_error(msg: String) =
    1.16            {
    1.17 -            Output.warning("Ignoring bad database: " +
    1.18 +            progress.echo_warning("Ignoring bad database: " +
    1.19                database.expand + (if (msg == "") "" else "\n" + msg))
    1.20              no_timings
    1.21            }
    1.22 @@ -63,12 +64,12 @@
    1.23        }
    1.24      }
    1.25  
    1.26 -    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
    1.27 +    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
    1.28      {
    1.29        val graph = sessions.build_graph
    1.30        val names = graph.keys
    1.31  
    1.32 -      val timings = names.map(name => (name, load_timings(store, name)))
    1.33 +      val timings = names.map(name => (name, load_timings(progress, store, name)))
    1.34        val command_timings =
    1.35          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    1.36        val session_timing =
    1.37 @@ -380,7 +381,7 @@
    1.38      /* main build process */
    1.39  
    1.40      val store = Sessions.store(system_mode)
    1.41 -    val queue = Queue(selected_sessions, store)
    1.42 +    val queue = Queue(progress, selected_sessions, store)
    1.43  
    1.44      store.prepare_output()
    1.45  
    1.46 @@ -683,7 +684,7 @@
    1.47            clean_build = clean_build,
    1.48            dirs = dirs,
    1.49            select_dirs = select_dirs,
    1.50 -          numa_shuffling = NUMA.enabled_warning(numa_shuffling),
    1.51 +          numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
    1.52            max_jobs = max_jobs,
    1.53            list_files = list_files,
    1.54            check_keywords = check_keywords,