tuned;
authorwenzelm
Fri Jul 27 13:33:34 2012 +0200 (2012-07-27)
changeset 48547b3b092d0a9fe
parent 48546 f81cf2fcd3a0
child 48548 49afe0e92163
tuned;
src/Pure/System/build.scala
     1.1 --- a/src/Pure/System/build.scala	Fri Jul 27 13:17:12 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 13:33:34 2012 +0200
     1.3 @@ -472,70 +472,71 @@
     1.4        results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] =
     1.5      {
     1.6        if (pending.is_empty) results
     1.7 -      else if (running.exists({ case (_, job) => job.is_finished }))
     1.8 -      { // finish job
     1.9 -        val (name, job) = running.find({ case (_, job) => job.is_finished }).get
    1.10 +      else
    1.11 +        running.find({ case (_, job) => job.is_finished }) match {
    1.12 +          case Some((name, job)) =>
    1.13 +            // finish job
    1.14  
    1.15 -        val (out, err, rc) = job.join
    1.16 -        echo(Library.trim_line(err))
    1.17 +            val (out, err, rc) = job.join
    1.18 +            echo(Library.trim_line(err))
    1.19  
    1.20 -        if (rc == 0) {
    1.21 -          val sources = make_stamp(name)
    1.22 -          val heap = heap_stamp(job.output_path)
    1.23 -          File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
    1.24 -        }
    1.25 -        else {
    1.26 -          File.write(output_dir + log(name), out)
    1.27 -          echo(name + " FAILED")
    1.28 -          echo("(see also " + log(name).file.toString + ")")
    1.29 -          val lines = split_lines(out)
    1.30 -          val tail = lines.drop(lines.length - 20 max 0)
    1.31 -          echo("\n" + cat_lines(tail))
    1.32 -        }
    1.33 -        loop(pending - name, running - name, results + (name -> (false, rc)))
    1.34 -      }
    1.35 -      else if (running.size < (max_jobs max 1))
    1.36 -      { // check/start next job
    1.37 -        pending.dequeue(running.isDefinedAt(_)) match {
    1.38 -          case Some((name, info)) =>
    1.39 -            val parent_result = info.parent.map(results(_))
    1.40 -            val parent_current = parent_result.forall(_._1)
    1.41 -            val parent_ok = parent_result.forall(_._2 == 0)
    1.42 +            if (rc == 0) {
    1.43 +              val sources = make_stamp(name)
    1.44 +              val heap = heap_stamp(job.output_path)
    1.45 +              File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
    1.46 +            }
    1.47 +            else {
    1.48 +              File.write(output_dir + log(name), out)
    1.49 +              echo(name + " FAILED")
    1.50 +              echo("(see also " + log(name).file.toString + ")")
    1.51 +              val lines = split_lines(out)
    1.52 +              val tail = lines.drop(lines.length - 20 max 0)
    1.53 +              echo("\n" + cat_lines(tail))
    1.54 +            }
    1.55 +            loop(pending - name, running - name, results + (name -> (false, rc)))
    1.56  
    1.57 -            val output = output_dir + Path.basic(name)
    1.58 -            val do_output = build_heap || queue.is_inner(name)
    1.59 +          case None if (running.size < (max_jobs max 1)) =>
    1.60 +            // check/start next job
    1.61 +            pending.dequeue(running.isDefinedAt(_)) match {
    1.62 +              case Some((name, info)) =>
    1.63 +                val parent_result = info.parent.map(results(_))
    1.64 +                val parent_current = parent_result.forall(_._1)
    1.65 +                val parent_ok = parent_result.forall(_._2 == 0)
    1.66  
    1.67 -            val current =
    1.68 -            {
    1.69 -              input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
    1.70 -                case Some(dir) =>
    1.71 -                  check_stamps(dir, name) match {
    1.72 -                    case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
    1.73 +                val output = output_dir + Path.basic(name)
    1.74 +                val do_output = build_heap || queue.is_inner(name)
    1.75 +
    1.76 +                val current =
    1.77 +                {
    1.78 +                  input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
    1.79 +                    case Some(dir) =>
    1.80 +                      check_stamps(dir, name) match {
    1.81 +                        case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
    1.82 +                        case None => false
    1.83 +                      }
    1.84                      case None => false
    1.85                    }
    1.86 -                case None => false
    1.87 -              }
    1.88 -            }
    1.89 -            val all_current = current && parent_current
    1.90 +                }
    1.91 +                val all_current = current && parent_current
    1.92  
    1.93 -            if (all_current)
    1.94 -              loop(pending - name, running, results + (name -> (true, 0)))
    1.95 -            else if (no_build)
    1.96 -              loop(pending - name, running, results + (name -> (false, 1)))
    1.97 -            else if (parent_ok) {
    1.98 -              echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.99 -              val job =
   1.100 -                start_job(name, info, output, do_output, info.options, verbose, browser_info)
   1.101 -              loop(pending, running + (name -> job), results)
   1.102 -            }
   1.103 -            else {
   1.104 -              echo(name + " CANCELLED")
   1.105 -              loop(pending - name, running, results + (name -> (false, 1)))
   1.106 +                if (all_current)
   1.107 +                  loop(pending - name, running, results + (name -> (true, 0)))
   1.108 +                else if (no_build)
   1.109 +                  loop(pending - name, running, results + (name -> (false, 1)))
   1.110 +                else if (parent_ok) {
   1.111 +                  echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.112 +                  val job =
   1.113 +                    start_job(name, info, output, do_output, info.options, verbose, browser_info)
   1.114 +                  loop(pending, running + (name -> job), results)
   1.115 +                }
   1.116 +                else {
   1.117 +                  echo(name + " CANCELLED")
   1.118 +                  loop(pending - name, running, results + (name -> (false, 1)))
   1.119 +                }
   1.120 +              case None => sleep(); loop(pending, running, results)
   1.121              }
   1.122            case None => sleep(); loop(pending, running, results)
   1.123          }
   1.124 -      }
   1.125 -      else { sleep(); loop(pending, running, results) }
   1.126      }
   1.127  
   1.128      val results = loop(queue, Map.empty, Map.empty)