# HG changeset patch
# User wenzelm
# Date 1343388814 -7200
# Node ID b3b092d0a9fe2b9684c6b86a0ff3f6faef6c7c9a
# Parent  f81cf2fcd3a07a1aad0f7253c2ad3de2b8f6ff0a
tuned;

diff -r f81cf2fcd3a0 -r b3b092d0a9fe src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 27 13:17:12 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 27 13:33:34 2012 +0200
@@ -472,70 +472,71 @@
       results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] =
     {
       if (pending.is_empty) results
-      else if (running.exists({ case (_, job) => job.is_finished }))
-      { // finish job
-        val (name, job) = running.find({ case (_, job) => job.is_finished }).get
+      else
+        running.find({ case (_, job) => job.is_finished }) match {
+          case Some((name, job)) =>
+            // finish job
 
-        val (out, err, rc) = job.join
-        echo(Library.trim_line(err))
+            val (out, err, rc) = job.join
+            echo(Library.trim_line(err))
 
-        if (rc == 0) {
-          val sources = make_stamp(name)
-          val heap = heap_stamp(job.output_path)
-          File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
-        }
-        else {
-          File.write(output_dir + log(name), out)
-          echo(name + " FAILED")
-          echo("(see also " + log(name).file.toString + ")")
-          val lines = split_lines(out)
-          val tail = lines.drop(lines.length - 20 max 0)
-          echo("\n" + cat_lines(tail))
-        }
-        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 parent_result = info.parent.map(results(_))
-            val parent_current = parent_result.forall(_._1)
-            val parent_ok = parent_result.forall(_._2 == 0)
+            if (rc == 0) {
+              val sources = make_stamp(name)
+              val heap = heap_stamp(job.output_path)
+              File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
+            }
+            else {
+              File.write(output_dir + log(name), out)
+              echo(name + " FAILED")
+              echo("(see also " + log(name).file.toString + ")")
+              val lines = split_lines(out)
+              val tail = lines.drop(lines.length - 20 max 0)
+              echo("\n" + cat_lines(tail))
+            }
+            loop(pending - name, running - name, results + (name -> (false, rc)))
 
-            val output = output_dir + Path.basic(name)
-            val do_output = build_heap || queue.is_inner(name)
+          case None if (running.size < (max_jobs max 1)) =>
+            // check/start next job
+            pending.dequeue(running.isDefinedAt(_)) match {
+              case Some((name, info)) =>
+                val parent_result = info.parent.map(results(_))
+                val parent_current = parent_result.forall(_._1)
+                val parent_ok = parent_result.forall(_._2 == 0)
 
-            val current =
-            {
-              input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
-                case Some(dir) =>
-                  check_stamps(dir, name) match {
-                    case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
+                val output = output_dir + Path.basic(name)
+                val do_output = build_heap || queue.is_inner(name)
+
+                val current =
+                {
+                  input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
+                    case Some(dir) =>
+                      check_stamps(dir, name) match {
+                        case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
+                        case None => false
+                      }
                     case None => false
                   }
-                case None => false
-              }
-            }
-            val all_current = current && parent_current
+                }
+                val all_current = current && parent_current
 
-            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, verbose, browser_info)
-              loop(pending, running + (name -> job), results)
-            }
-            else {
-              echo(name + " CANCELLED")
-              loop(pending - name, running, results + (name -> (false, 1)))
+                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, verbose, browser_info)
+                  loop(pending, running + (name -> job), results)
+                }
+                else {
+                  echo(name + " CANCELLED")
+                  loop(pending - name, running, results + (name -> (false, 1)))
+                }
+              case None => sleep(); loop(pending, running, results)
             }
           case None => sleep(); loop(pending, running, results)
         }
-      }
-      else { sleep(); loop(pending, running, results) }
     }
 
     val results = loop(queue, Map.empty, Map.empty)