1.1 --- a/src/Pure/System/build.scala	Fri Jul 20 12:27:25 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 12:45:12 2012 +0200
     1.3 @@ -156,6 +156,8 @@
     1.4    private val ROOT = Path.explode("ROOT")
     1.5    private val SESSIONS = Path.explode("etc/sessions")
     1.6  
     1.7 +  private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
     1.8 +
     1.9    private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
    1.10    {
    1.11      (queue /: Parser.parse_entries(root))((queue1, entry) =>
    1.12 @@ -163,7 +165,7 @@
    1.13          if (entry.name == "") error("Bad session name")
    1.14  
    1.15          val full_name =
    1.16 -          if (entry.name == "RAW" || entry.name == "Pure") {
    1.17 +          if (is_pure(entry.name)) {
    1.18              if (entry.parent.isDefined) error("Illegal parent session")
    1.19              else entry.name
    1.20            }
    1.21 @@ -240,6 +242,16 @@
    1.22  
    1.23    /** build **/
    1.24  
    1.25 +  private def build_job(build_images: Boolean,  // FIXME
    1.26 +    key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
    1.27 +  {
    1.28 +    val cwd = Isabelle_System.platform_file(info.dir)
    1.29 +    val script =
    1.30 +      if (is_pure(key.name)) "./build " + key.name
    1.31 +      else """echo "Bad session" >&2; exit 2"""
    1.32 +    new Isabelle_System.Bash_Job(cwd, null, script)
    1.33 +  }
    1.34 +
    1.35    def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    1.36      more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
    1.37    {
    1.38 @@ -254,8 +266,13 @@
    1.39        if (all_sessions) full_queue
    1.40        else full_queue.required(sessions)
    1.41  
    1.42 -    for ((key, info) <- required_queue.topological_order)
    1.43 -      println(key.name + " in " + info.dir)
    1.44 +    for ((key, info) <- required_queue.topological_order) {
    1.45 +      if (list_only) println(key.name + " in " + info.dir)
    1.46 +      else {
    1.47 +        val (out, err, rc) = build_job(build_images, key, info).join
    1.48 +        java.lang.System.err.print(err)
    1.49 +      }
    1.50 +    }
    1.51  
    1.52      0
    1.53    }