minimal build_job;
authorwenzelm
Fri, 20 Jul 2012 12:45:12 +0200
changeset 48364 9091b659d7b6
parent 48363 cf081b7042d2
child 48365 d88aefda01c4
minimal build_job;
src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 20 12:27:25 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 12:45:12 2012 +0200
@@ -156,6 +156,8 @@
   private val ROOT = Path.explode("ROOT")
   private val SESSIONS = Path.explode("etc/sessions")
 
+  private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
+
   private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
   {
     (queue /: Parser.parse_entries(root))((queue1, entry) =>
@@ -163,7 +165,7 @@
         if (entry.name == "") error("Bad session name")
 
         val full_name =
-          if (entry.name == "RAW" || entry.name == "Pure") {
+          if (is_pure(entry.name)) {
             if (entry.parent.isDefined) error("Illegal parent session")
             else entry.name
           }
@@ -240,6 +242,16 @@
 
   /** build **/
 
+  private def build_job(build_images: Boolean,  // FIXME
+    key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
+  {
+    val cwd = Isabelle_System.platform_file(info.dir)
+    val script =
+      if (is_pure(key.name)) "./build " + key.name
+      else """echo "Bad session" >&2; exit 2"""
+    new Isabelle_System.Bash_Job(cwd, null, script)
+  }
+
   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   {
@@ -254,8 +266,13 @@
       if (all_sessions) full_queue
       else full_queue.required(sessions)
 
-    for ((key, info) <- required_queue.topological_order)
-      println(key.name + " in " + info.dir)
+    for ((key, info) <- required_queue.topological_order) {
+      if (list_only) println(key.name + " in " + info.dir)
+      else {
+        val (out, err, rc) = build_job(build_images, key, info).join
+        java.lang.System.err.print(err)
+      }
+    }
 
     0
   }