src/Pure/Tools/build.scala
changeset 50707 5b2bf7611662
parent 50686 d703e3aafa8c
child 50713 dae523e6198b
     1.1 --- a/src/Pure/Tools/build.scala	Thu Jan 03 15:13:11 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 03 20:42:18 2013 +0100
     1.3 @@ -412,7 +412,7 @@
     1.4  
     1.5    /* jobs */
     1.6  
     1.7 -  private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
     1.8 +  private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
     1.9      verbose: Boolean, browser_info: Path)
    1.10    {
    1.11      // global browser info dir
    1.12 @@ -515,6 +515,8 @@
    1.13    private def log(name: String): Path = LOG + Path.basic(name)
    1.14    private def log_gz(name: String): Path = log(name).ext("gz")
    1.15  
    1.16 +  private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    1.17 +
    1.18    private def sources_stamp(digests: List[SHA1.Digest]): String =
    1.19      digests.map(_.toString).sorted.mkString("sources: ", " ", "")
    1.20  
    1.21 @@ -600,7 +602,7 @@
    1.22      }
    1.23  
    1.24      // scheduler loop
    1.25 -    case class Result(current: Boolean, heap: String, rc: Int)
    1.26 +    case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
    1.27  
    1.28      def sleep(): Unit = Thread.sleep(500)
    1.29  
    1.30 @@ -620,9 +622,10 @@
    1.31              //{{{ finish job
    1.32  
    1.33              val (out, err, rc) = job.join
    1.34 +            val out_lines = split_lines(out)
    1.35              progress.echo(Library.trim_line(err))
    1.36  
    1.37 -            val heap =
    1.38 +            val (parent_path, heap) =
    1.39                if (rc == 0) {
    1.40                  (output_dir + log(name)).file.delete
    1.41  
    1.42 @@ -631,7 +634,13 @@
    1.43                  File.write_gzip(output_dir + log_gz(name),
    1.44                    sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
    1.45  
    1.46 -                heap
    1.47 +                val parent_path =
    1.48 +                  if (job.info.options.bool("browser_info"))
    1.49 +                    out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
    1.50 +                      line.substring(SESSION_PARENT_PATH.length))
    1.51 +                  else None
    1.52 +
    1.53 +                (parent_path, heap)
    1.54                }
    1.55                else {
    1.56                  (output_dir + Path.basic(name)).file.delete
    1.57 @@ -641,14 +650,14 @@
    1.58                  progress.echo(name + " FAILED")
    1.59                  if (rc != 130) {
    1.60                    progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
    1.61 -                  val lines = split_lines(out)
    1.62 -                  val tail = lines.drop(lines.length - 20 max 0)
    1.63 +                  val tail = out_lines.drop(out_lines.length - 20 max 0)
    1.64                    progress.echo("\n" + cat_lines(tail))
    1.65                  }
    1.66  
    1.67 -                no_heap
    1.68 +                (None, no_heap)
    1.69                }
    1.70 -            loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
    1.71 +            loop(pending - name, running - name,
    1.72 +              results + (name -> Result(false, parent_path, heap, rc)))
    1.73              //}}}
    1.74            case None if (running.size < (max_jobs max 1)) =>
    1.75              //{{{ check/start next job
    1.76 @@ -656,7 +665,7 @@
    1.77                case Some((name, info)) =>
    1.78                  val parent_result =
    1.79                    info.parent match {
    1.80 -                    case None => Result(true, no_heap, 0)
    1.81 +                    case None => Result(true, None, no_heap, 0)
    1.82                      case Some(parent) => results(parent)
    1.83                    }
    1.84                  val output = output_dir + Path.basic(name)
    1.85 @@ -679,10 +688,10 @@
    1.86                  val all_current = current && parent_result.current
    1.87  
    1.88                  if (all_current)
    1.89 -                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
    1.90 +                  loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
    1.91                  else if (no_build) {
    1.92                    if (verbose) progress.echo("Skipping " + name + " ...")
    1.93 -                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
    1.94 +                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
    1.95                  }
    1.96                  else if (parent_result.rc == 0) {
    1.97                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.98 @@ -691,7 +700,7 @@
    1.99                  }
   1.100                  else {
   1.101                    progress.echo(name + " CANCELLED")
   1.102 -                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   1.103 +                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
   1.104                  }
   1.105                case None => sleep(); loop(pending, running, results)
   1.106              }
   1.107 @@ -703,10 +712,17 @@
   1.108      val results =
   1.109        if (deps.is_empty) {
   1.110          progress.echo("### Nothing to build")
   1.111 -        Map.empty
   1.112 +        Map.empty[String, Result]
   1.113        }
   1.114        else loop(queue, Map.empty, Map.empty)
   1.115  
   1.116 +    val session_entries =
   1.117 +      (for ((name, res) <- results.iterator if res.parent_path.isDefined)
   1.118 +        yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
   1.119 +          { case (p, es) => (p, es.map(_._2).sorted) })
   1.120 +    for ((p, names) <- session_entries)
   1.121 +      Present.update_index(browser_info + Path.explode(p), names)
   1.122 +
   1.123      val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   1.124      if (rc != 0 && (verbose || !no_build)) {
   1.125        val unfinished =