1.1 --- a/src/Pure/General/file.scala	Sat Jul 21 12:57:31 2012 +0200
     1.2 +++ b/src/Pure/General/file.scala	Sat Jul 21 16:41:55 2012 +0200
     1.3 @@ -83,10 +83,16 @@
     1.4  
     1.5    /* misc */
     1.6  
     1.7 -  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
     1.8 +  def tmp_file(prefix: String): JFile =
     1.9    {
    1.10      val file = JFile.createTempFile(prefix, null)
    1.11      file.deleteOnExit
    1.12 +    file
    1.13 +  }
    1.14 +
    1.15 +  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    1.16 +  {
    1.17 +    val file = tmp_file(prefix)
    1.18      try { body(file) } finally { file.delete }
    1.19    }
    1.20  

     2.1 --- a/src/Pure/IsaMakefile	Sat Jul 21 12:57:31 2012 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Sat Jul 21 16:41:55 2012 +0200
     2.3 @@ -189,6 +189,7 @@
     2.4    Syntax/syntax_trans.ML				\
     2.5    Syntax/term_position.ML				\
     2.6    System/invoke_scala.ML				\
     2.7 +  System/build.ML					\
     2.8    System/isabelle_process.ML				\
     2.9    System/isabelle_system.ML				\
    2.10    System/isar.ML					\

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

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/System/build.ML	Sat Jul 21 16:41:55 2012 +0200
     4.3 @@ -0,0 +1,29 @@
     4.4 +(*  Title:      Pure/System/build.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Build Isabelle sessions.
     4.8 +*)
     4.9 +
    4.10 +signature BUILD =
    4.11 +sig
    4.12 +  val build: string -> unit
    4.13 +end;
    4.14 +
    4.15 +structure Build: BUILD =
    4.16 +struct
    4.17 +
    4.18 +fun build args_file =
    4.19 +  let
    4.20 +    val (build_images, (parent, (name, theories))) =
    4.21 +      File.read (Path.explode args_file) |> YXML.parse_body |>
    4.22 +        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
    4.23 +
    4.24 +    val _ = Session.init false parent name;  (* FIXME reset!? *)
    4.25 +    val _ = Thy_Info.use_thys theories;
    4.26 +    val _ = Session.finish ();
    4.27 +
    4.28 +    val _ = if build_images then () else quit ();
    4.29 +  in () end
    4.30 +  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    4.31 +
    4.32 +end;

     5.1 --- a/src/Pure/System/build.scala	Sat Jul 21 12:57:31 2012 +0200
     5.2 +++ b/src/Pure/System/build.scala	Sat Jul 21 16:41:55 2012 +0200
     5.3 @@ -40,9 +40,10 @@
     5.4  
     5.5      sealed case class Info(
     5.6        dir: Path,
     5.7 +      parent: Option[String],
     5.8        description: String,
     5.9        options: Options,
    5.10 -      theories: List[(Options, String)],
    5.11 +      theories: List[(Options, List[String])],
    5.12        files: List[String])
    5.13  
    5.14      object Queue
    5.15 @@ -56,7 +57,7 @@
    5.16      {
    5.17        def defined(name: String): Boolean = keys.isDefinedAt(name)
    5.18  
    5.19 -      def + (key: Key, info: Info, parent: Option[String]): Queue =
    5.20 +      def + (key: Key, info: Info): Queue =
    5.21        {
    5.22          val keys1 =
    5.23            if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    5.24 @@ -64,7 +65,7 @@
    5.25  
    5.26          val graph1 =
    5.27            try {
    5.28 -            graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
    5.29 +            graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
    5.30            }
    5.31            catch {
    5.32              case exn: Graph.Cycles[_] =>
    5.33 @@ -184,10 +185,11 @@
    5.34            }
    5.35  
    5.36          val key = Session.Key(full_name, entry.order)
    5.37 -        val info = Session.Info(dir + path, entry.description, entry.options,
    5.38 -          entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
    5.39 +        val info =
    5.40 +          Session.Info(dir + path, entry.parent,
    5.41 +            entry.description, entry.options, entry.theories, entry.files)
    5.42  
    5.43 -        queue1 + (key, info, entry.parent)
    5.44 +        queue1 + (key, info)
    5.45        }
    5.46        catch {
    5.47          case ERROR(msg) =>
    5.48 @@ -244,14 +246,57 @@
    5.49    private def echo(msg: String) { java.lang.System.out.println(msg) }
    5.50    private def echo_n(msg: String) { java.lang.System.out.print(msg) }
    5.51  
    5.52 -  private def build_job(build_images: Boolean,  // FIXME
    5.53 -    key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
    5.54 +  class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
    5.55    {
    5.56 +    private val args_file = File.tmp_file("args")
    5.57 +    private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    5.58 +    File.write(args_file, args)
    5.59 +
    5.60 +    private val (thread, result) = Simple_Thread.future("build_job") {
    5.61 +      Isabelle_System.bash_env(cwd, env1, script)
    5.62 +    }
    5.63 +
    5.64 +    def terminate: Unit = thread.interrupt
    5.65 +    def is_finished: Boolean = result.is_finished
    5.66 +    def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
    5.67 +  }
    5.68 +
    5.69 +  private def build_job(build_images: Boolean, name: String, info: Session.Info): Build_Job =
    5.70 +  {
    5.71 +    val parent = info.parent.getOrElse("")
    5.72 +
    5.73      val cwd = info.dir.file
    5.74 +    val env = Map("INPUT" -> parent, "TARGET" -> name)
    5.75      val script =
    5.76 -      if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
    5.77 -      else """echo "Bad session" >&2; exit 2"""
    5.78 -    new Isabelle_System.Bash_Job(cwd, null, script)
    5.79 +      if (is_pure(name)) "./build " + (if (build_images) "-b " else "") + name
    5.80 +      else {
    5.81 +        """
    5.82 +        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    5.83 +        """ +
    5.84 +          (if (build_images)
    5.85 +            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
    5.86 +          else
    5.87 +            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
    5.88 +        """
    5.89 +        RC="$?"
    5.90 +
    5.91 +        . "$ISABELLE_HOME/lib/scripts/timestop.bash"
    5.92 +
    5.93 +        if [ "$RC" -eq 0 ]; then
    5.94 +          echo "Finished $TARGET ($TIMES_REPORT)" >&2
    5.95 +        fi
    5.96 +
    5.97 +        exit "$RC"
    5.98 +        """
    5.99 +      }
   5.100 +    val args_xml =
   5.101 +    {
   5.102 +      import XML.Encode._
   5.103 +      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
   5.104 +      pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
   5.105 +        build_images, (parent, (name, info.theories.map(_._2).flatten)))
   5.106 +    }
   5.107 +    new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
   5.108    }
   5.109  
   5.110    def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
   5.111 @@ -292,10 +337,10 @@
   5.112        {
   5.113          if (list_only) { echo(key.name + " in " + info.dir); 0 }
   5.114          else {
   5.115 -          if (build_images) echo("Building " + key.name + "...")
   5.116 -          else echo("Running " + key.name + "...")
   5.117 +          if (build_images) echo("Building " + key.name + " ...")
   5.118 +          else echo("Running " + key.name + " ...")
   5.119  
   5.120 -          val (out, err, rc) = build_job(build_images, key, info).join
   5.121 +          val (out, err, rc) = build_job(build_images, key.name, info).join
   5.122            echo_n(err)
   5.123  
   5.124            val log = log_dir + Path.basic(key.name)

     6.1 --- a/src/Pure/System/isabelle_system.scala	Sat Jul 21 12:57:31 2012 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Jul 21 16:41:55 2012 +0200
     6.3 @@ -260,17 +260,6 @@
     6.4  
     6.5    def bash(script: String): (String, String, Int) = bash_env(null, null, script)
     6.6  
     6.7 -  class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
     6.8 -  {
     6.9 -    private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
    6.10 -
    6.11 -    def terminate: Unit = thread.interrupt
    6.12 -    def is_finished: Boolean = result.is_finished
    6.13 -    def join: (String, String, Int) = result.join
    6.14 -
    6.15 -    override def toString: String = if (is_finished) join._3.toString else "<running>"
    6.16 -  }
    6.17 -
    6.18  
    6.19    /* system tools */
    6.20  

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