proper all_current, which regards parent status as well;
authorwenzelm
Thu, 26 Jul 2012 19:57:33 +0200
changeset 49543784c6f63d79c
parent 49542 4ee8d70cd5a3
child 49551 4e2ee88276d2
proper all_current, which regards parent status as well;
src/Pure/System/build.scala
     1.1 --- a/src/Pure/System/build.scala	Thu Jul 26 19:41:05 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 26 19:57:33 2012 +0200
     1.3 @@ -502,10 +502,12 @@
     1.4        { // check/start next job
     1.5          pending.dequeue(running.isDefinedAt(_)) match {
     1.6            case Some((name, info)) =>
     1.7 +            val parents_ok = info.parent.map(results(_)).forall(_ == 0)
     1.8 +
     1.9              val output = output_dir + Path.basic(name)
    1.10              val do_output = build_heap || queue.is_inner(name)
    1.11  
    1.12 -            val current =
    1.13 +            val all_current =
    1.14              {
    1.15                input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
    1.16                  case Some(dir) =>
    1.17 @@ -515,10 +517,11 @@
    1.18                    }
    1.19                  case None => false
    1.20                }
    1.21 -            }
    1.22 -            if (current || no_build)
    1.23 -              loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
    1.24 -            else if (info.parent.map(results(_)).forall(_ == 0)) {
    1.25 +            } && parents_ok
    1.26 +
    1.27 +            if (all_current || no_build)
    1.28 +              loop(pending - name, running, results + (name -> (if (all_current) 0 else 1)))
    1.29 +            else if (parents_ok) {
    1.30                echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.31                val job =
    1.32                  start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)