# HG changeset patch
# User wenzelm
# Date 1343332216 -7200
# Node ID ba0dd46b9214632280acbce4209f96d05527f3be
# Parent  4e2ee88276d22bc8c126d5e63549b93c134dbfa9
further refinement of current/all_current status, which needs to be propagated through the hierarchy (see also Thy_Info.require_thys);

diff -r 4e2ee88276d2 -r ba0dd46b9214 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 26 19:59:06 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 26 21:50:16 2012 +0200
@@ -473,7 +473,7 @@
     @tailrec def loop(
       pending: Session.Queue,
       running: Map[String, Job],
-      results: Map[String, Int]): Map[String, Int] =
+      results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] =
     {
       if (pending.is_empty) results
       else if (running.exists({ case (_, job) => job.is_finished }))
@@ -496,18 +496,20 @@
           val tail = lines.drop(lines.length - 20 max 0)
           echo("\n" + cat_lines(tail))
         }
-        loop(pending - name, running - name, results + (name -> rc))
+        loop(pending - name, running - name, results + (name -> (false, rc)))
       }
       else if (running.size < (max_jobs max 1))
       { // check/start next job
         pending.dequeue(running.isDefinedAt(_)) match {
           case Some((name, info)) =>
-            val parents_ok = info.parent.map(results(_)).forall(_ == 0)
+            val parent_result = info.parent.map(results(_))
+            val parent_current = parent_result.forall(_._1)
+            val parent_ok = parent_result.forall(_._2 == 0)
 
             val output = output_dir + Path.basic(name)
             val do_output = build_heap || queue.is_inner(name)
 
-            val all_current =
+            val current =
             {
               input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
                 case Some(dir) =>
@@ -517,11 +519,14 @@
                   }
                 case None => false
               }
-            } && parents_ok
+            }
+            val all_current = current && parent_current
 
-            if (all_current || no_build)
-              loop(pending - name, running, results + (name -> (if (all_current) 0 else 1)))
-            else if (parents_ok) {
+            if (all_current)
+              loop(pending - name, running, results + (name -> (true, 0)))
+            else if (no_build)
+              loop(pending - name, running, results + (name -> (false, 1)))
+            else if (parent_ok) {
               echo((if (do_output) "Building " else "Running ") + name + " ...")
               val job =
                 start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)
@@ -529,7 +534,7 @@
             }
             else {
               echo(name + " CANCELLED")
-              loop(pending - name, running, results + (name -> 1))
+              loop(pending - name, running, results + (name -> (false, 1)))
             }
           case None => sleep(); loop(pending, running, results)
         }
@@ -538,7 +543,7 @@
     }
 
     val results = loop(queue, Map.empty, Map.empty)
-    val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
+    val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
       val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
       echo("Unfinished session(s): " + commas(unfinished))