src/Pure/Tools/build.scala
changeset 65420 695d4e22345a
parent 65419 457e4fbed731
child 65422 b606c98e6d10
     1.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 10:47:25 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 11:50:49 2017 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5      def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     1.6      {
     1.7 -      val graph = sessions.graph
     1.8 +      val graph = sessions.build_graph
     1.9        val names = graph.keys
    1.10  
    1.11        val timings = names.map(name => (name, load_timings(store, name)))
    1.12 @@ -413,7 +413,7 @@
    1.13  
    1.14      // optional cleanup
    1.15      if (clean_build) {
    1.16 -      for (name <- full_sessions.graph.all_succs(selected)) {
    1.17 +      for (name <- full_sessions.build_descendants(selected)) {
    1.18          val files =
    1.19            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    1.20              map(store.output_dir + _).filter(_.is_file)
    1.21 @@ -519,7 +519,7 @@
    1.22              //{{{ check/start next job
    1.23              pending.dequeue(running.isDefinedAt(_)) match {
    1.24                case Some((name, info)) =>
    1.25 -                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
    1.26 +                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
    1.27                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    1.28  
    1.29                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)