1.1 --- a/src/Pure/System/build.scala	Sun Jul 22 12:26:41 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Sun Jul 22 21:59:14 2012 +0200
     1.3 @@ -41,10 +41,6 @@
     1.4  
     1.5      /* Info */
     1.6  
     1.7 -    sealed abstract class Status
     1.8 -    case object Pending extends Status
     1.9 -    case object Running extends Status
    1.10 -
    1.11      sealed case class Info(
    1.12        dir: Path,
    1.13        parent: Option[String],
    1.14 @@ -52,8 +48,7 @@
    1.15        options: Options,
    1.16        theories: List[(Options, List[Path])],
    1.17        files: List[Path],
    1.18 -      digest: SHA1.Digest,
    1.19 -      status: Status = Pending)
    1.20 +      digest: SHA1.Digest)
    1.21  
    1.22  
    1.23      /* Queue */
    1.24 @@ -269,6 +264,9 @@
    1.25    }
    1.26  
    1.27  
    1.28 +
    1.29 +  /** build **/
    1.30 +
    1.31    /* dependencies */
    1.32  
    1.33    sealed case class Node(
    1.34 @@ -314,28 +312,23 @@
    1.35        }))
    1.36  
    1.37  
    1.38 +  /* jobs */
    1.39  
    1.40 -  /** build **/
    1.41 -
    1.42 -  private def echo(msg: String) { java.lang.System.out.println(msg) }
    1.43 -  private def echo_n(msg: String) { java.lang.System.out.print(msg) }
    1.44 -
    1.45 -  class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
    1.46 +  private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
    1.47    {
    1.48      private val args_file = File.tmp_file("args")
    1.49      private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    1.50      File.write(args_file, args)
    1.51  
    1.52 -    private val (thread, result) = Simple_Thread.future("build_job") {
    1.53 -      Isabelle_System.bash_env(cwd, env1, script)
    1.54 -    }
    1.55 +    private val (thread, result) =
    1.56 +      Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
    1.57  
    1.58      def terminate: Unit = thread.interrupt
    1.59      def is_finished: Boolean = result.is_finished
    1.60      def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
    1.61    }
    1.62  
    1.63 -  private def build_job(save: Boolean, name: String, info: Session.Info): Build_Job =
    1.64 +  private def start_job(save: Boolean, name: String, info: Session.Info): Job =
    1.65    {
    1.66      val parent = info.parent.getOrElse("")
    1.67  
    1.68 @@ -369,9 +362,15 @@
    1.69        pair(bool, pair(string, pair(string, list(string))))(
    1.70          save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
    1.71      }
    1.72 -    new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
    1.73 +    new Job(cwd, env, script, YXML.string_of_body(args_xml))
    1.74    }
    1.75  
    1.76 +
    1.77 +  /* Scala entry point */
    1.78 +
    1.79 +  private def echo(msg: String) { java.lang.System.out.println(msg) }
    1.80 +  private def echo_n(msg: String) { java.lang.System.out.print(msg) }
    1.81 +
    1.82    def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    1.83      more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
    1.84    {
    1.85 @@ -397,7 +396,7 @@
    1.86      val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
    1.87      log_dir.file.mkdirs()
    1.88  
    1.89 -    // run jobs
    1.90 +
    1.91      val rcs =
    1.92        for ((name, info) <- queue.topological_order) yield
    1.93        {
    1.94 @@ -406,7 +405,7 @@
    1.95            val save = build_images || queue.is_inner(name)
    1.96            echo((if (save) "Building " else "Running ") + name + " ...")
    1.97  
    1.98 -          val (out, err, rc) = build_job(save, name, info).join
    1.99 +          val (out, err, rc) = start_job(save, name, info).join
   1.100            echo_n(err)
   1.101  
   1.102            val log = log_dir + Path.basic(name)