some actual build function on ML side;
further imitation of "usedir" shell script;

--- a/src/Pure/General/file.scala	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/General/file.scala	Sat Jul 21 16:41:55 2012 +0200
@@ -83,10 +83,16 @@
 
   /* misc */
 
-  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+  def tmp_file(prefix: String): JFile =
   {
     val file = JFile.createTempFile(prefix, null)
     file.deleteOnExit
+    file
+  }
+
+  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+  {
+    val file = tmp_file(prefix)
     try { body(file) } finally { file.delete }
   }
 

--- a/src/Pure/IsaMakefile	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/IsaMakefile	Sat Jul 21 16:41:55 2012 +0200
@@ -189,6 +189,7 @@
   Syntax/syntax_trans.ML				\
   Syntax/term_position.ML				\
   System/invoke_scala.ML				\
+  System/build.ML					\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
   System/isar.ML					\

--- a/src/Pure/ROOT.ML	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 21 16:41:55 2012 +0200
@@ -268,6 +268,7 @@
 (* Isabelle/Isar system *)
 
 use "System/session.ML";
+use "System/build.ML";
 use "System/system_channel.ML";
 use "System/isabelle_process.ML";
 use "System/invoke_scala.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/build.ML	Sat Jul 21 16:41:55 2012 +0200
@@ -0,0 +1,29 @@
+(*  Title:      Pure/System/build.ML
+    Author:     Makarius
+
+Build Isabelle sessions.
+*)
+
+signature BUILD =
+sig
+  val build: string -> unit
+end;
+
+structure Build: BUILD =
+struct
+
+fun build args_file =
+  let
+    val (build_images, (parent, (name, theories))) =
+      File.read (Path.explode args_file) |> YXML.parse_body |>
+        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
+
+    val _ = Session.init false parent name;  (* FIXME reset!? *)
+    val _ = Thy_Info.use_thys theories;
+    val _ = Session.finish ();
+
+    val _ = if build_images then () else quit ();
+  in () end
+  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
+
+end;

--- a/src/Pure/System/build.scala	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/System/build.scala	Sat Jul 21 16:41:55 2012 +0200
@@ -40,9 +40,10 @@
 
     sealed case class Info(
       dir: Path,
+      parent: Option[String],
       description: String,
       options: Options,
-      theories: List[(Options, String)],
+      theories: List[(Options, List[String])],
       files: List[String])
 
     object Queue
@@ -56,7 +57,7 @@
     {
       def defined(name: String): Boolean = keys.isDefinedAt(name)
 
-      def + (key: Key, info: Info, parent: Option[String]): Queue =
+      def + (key: Key, info: Info): Queue =
       {
         val keys1 =
           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
@@ -64,7 +65,7 @@
 
         val graph1 =
           try {
-            graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
+            graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
           }
           catch {
             case exn: Graph.Cycles[_] =>
@@ -184,10 +185,11 @@
           }
 
         val key = Session.Key(full_name, entry.order)
-        val info = Session.Info(dir + path, entry.description, entry.options,
-          entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
+        val info =
+          Session.Info(dir + path, entry.parent,
+            entry.description, entry.options, entry.theories, entry.files)
 
-        queue1 + (key, info, entry.parent)
+        queue1 + (key, info)
       }
       catch {
         case ERROR(msg) =>
@@ -244,14 +246,57 @@
   private def echo(msg: String) { java.lang.System.out.println(msg) }
   private def echo_n(msg: String) { java.lang.System.out.print(msg) }
 
-  private def build_job(build_images: Boolean,  // FIXME
-    key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
+  class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
   {
+    private val args_file = File.tmp_file("args")
+    private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
+    File.write(args_file, args)
+
+    private val (thread, result) = Simple_Thread.future("build_job") {
+      Isabelle_System.bash_env(cwd, env1, script)
+    }
+
+    def terminate: Unit = thread.interrupt
+    def is_finished: Boolean = result.is_finished
+    def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
+  }
+
+  private def build_job(build_images: Boolean, name: String, info: Session.Info): Build_Job =
+  {
+    val parent = info.parent.getOrElse("")
+
     val cwd = info.dir.file
+    val env = Map("INPUT" -> parent, "TARGET" -> name)
     val script =
-      if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
-      else """echo "Bad session" >&2; exit 2"""
-    new Isabelle_System.Bash_Job(cwd, null, script)
+      if (is_pure(name)) "./build " + (if (build_images) "-b " else "") + name
+      else {
+        """
+        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
+        """ +
+          (if (build_images)
+            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
+          else
+            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
+        """
+        RC="$?"
+
+        . "$ISABELLE_HOME/lib/scripts/timestop.bash"
+
+        if [ "$RC" -eq 0 ]; then
+          echo "Finished $TARGET ($TIMES_REPORT)" >&2
+        fi
+
+        exit "$RC"
+        """
+      }
+    val args_xml =
+    {
+      import XML.Encode._
+      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
+      pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
+        build_images, (parent, (name, info.theories.map(_._2).flatten)))
+    }
+    new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
   }
 
   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
@@ -292,10 +337,10 @@
       {
         if (list_only) { echo(key.name + " in " + info.dir); 0 }
         else {
-          if (build_images) echo("Building " + key.name + "...")
-          else echo("Running " + key.name + "...")
+          if (build_images) echo("Building " + key.name + " ...")
+          else echo("Running " + key.name + " ...")
 
-          val (out, err, rc) = build_job(build_images, key, info).join
+          val (out, err, rc) = build_job(build_images, key.name, info).join
           echo_n(err)
 
           val log = log_dir + Path.basic(key.name)

--- a/src/Pure/System/isabelle_system.scala	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jul 21 16:41:55 2012 +0200
@@ -260,17 +260,6 @@
 
   def bash(script: String): (String, String, Int) = bash_env(null, null, script)
 
-  class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
-  {
-    private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
-
-    def terminate: Unit = thread.interrupt
-    def is_finished: Boolean = result.is_finished
-    def join: (String, String, Int) = result.join
-
-    override def toString: String = if (is_finished) join._3.toString else "<running>"
-  }
-
 
   /* system tools */
 

--- a/src/Pure/System/session.ML	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/System/session.ML	Sat Jul 21 16:41:55 2012 +0200
@@ -9,6 +9,7 @@
   val id: unit -> string list
   val name: unit -> string
   val welcome: unit -> string
+  val init: bool -> string -> string -> unit
   val use_dir: string -> string -> bool -> string list -> bool -> bool ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit