1.1 --- a/src/Pure/System/build.ML Sat Jul 21 16:41:55 2012 +0200
1.2 +++ b/src/Pure/System/build.ML Sat Jul 21 17:49:22 2012 +0200
1.3 @@ -14,7 +14,7 @@
1.4
1.5 fun build args_file =
1.6 let
1.7 - val (build_images, (parent, (name, theories))) =
1.8 + val (save, (parent, (name, theories))) =
1.9 File.read (Path.explode args_file) |> YXML.parse_body |>
1.10 let open XML.Decode in pair bool (pair string (pair string (list string))) end;
1.11
1.12 @@ -22,7 +22,7 @@
1.13 val _ = Thy_Info.use_thys theories;
1.14 val _ = Session.finish ();
1.15
1.16 - val _ = if build_images then () else quit ();
1.17 + val _ = if save then () else quit ();
1.18 in () end
1.19 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
1.20
2.1 --- a/src/Pure/System/build.scala Sat Jul 21 16:41:55 2012 +0200
2.2 +++ b/src/Pure/System/build.scala Sat Jul 21 17:49:22 2012 +0200
2.3 @@ -57,6 +57,8 @@
2.4 {
2.5 def defined(name: String): Boolean = keys.isDefinedAt(name)
2.6
2.7 + def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
2.8 +
2.9 def + (key: Key, info: Info): Queue =
2.10 {
2.11 val keys1 =
2.12 @@ -222,7 +224,8 @@
2.13 })
2.14 }
2.15
2.16 - def find_sessions(more_dirs: List[Path]): Session.Queue =
2.17 + def find_sessions(all_sessions: Boolean, sessions: List[String],
2.18 + more_dirs: List[Path]): Session.Queue =
2.19 {
2.20 var queue = Session.Queue.empty
2.21
2.22 @@ -236,7 +239,12 @@
2.23
2.24 for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
2.25
2.26 - queue
2.27 + sessions.filter(name => !queue.defined(name)) match {
2.28 + case Nil =>
2.29 + case bad => error("Undefined session(s): " + commas_quote(bad))
2.30 + }
2.31 +
2.32 + if (all_sessions) queue else queue.required(sessions)
2.33 }
2.34
2.35
2.36 @@ -261,19 +269,19 @@
2.37 def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
2.38 }
2.39
2.40 - private def build_job(build_images: Boolean, name: String, info: Session.Info): Build_Job =
2.41 + private def build_job(save: Boolean, name: String, info: Session.Info): Build_Job =
2.42 {
2.43 val parent = info.parent.getOrElse("")
2.44
2.45 val cwd = info.dir.file
2.46 val env = Map("INPUT" -> parent, "TARGET" -> name)
2.47 val script =
2.48 - if (is_pure(name)) "./build " + (if (build_images) "-b " else "") + name
2.49 + if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
2.50 else {
2.51 """
2.52 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
2.53 """ +
2.54 - (if (build_images)
2.55 + (if (save)
2.56 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
2.57 else
2.58 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
2.59 @@ -294,28 +302,20 @@
2.60 import XML.Encode._
2.61 def symbol_string: T[String] = (s => string(Symbol.encode(s)))
2.62 pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
2.63 - build_images, (parent, (name, info.theories.map(_._2).flatten)))
2.64 + save, (parent, (name, info.theories.map(_._2).flatten)))
2.65 }
2.66 new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
2.67 }
2.68
2.69 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
2.70 - more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
2.71 + more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
2.72 {
2.73 - val full_queue = find_sessions(more_dirs)
2.74 - val build_options = (Options.init() /: options)(_.define_simple(_))
2.75 + val options = (Options.init() /: more_options)(_.define_simple(_))
2.76 + val queue = find_sessions(all_sessions, sessions, more_dirs)
2.77
2.78 - sessions.filter(name => !full_queue.defined(name)) match {
2.79 - case Nil =>
2.80 - case bad => error("Undefined session(s): " + commas_quote(bad))
2.81 - }
2.82 -
2.83 - val required_queue =
2.84 - if (all_sessions) full_queue
2.85 - else full_queue.required(sessions)
2.86
2.87 // prepare browser info dir
2.88 - if (build_options.bool("browser_info") &&
2.89 + if (options.bool("browser_info") &&
2.90 !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
2.91 {
2.92 Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
2.93 @@ -333,23 +333,25 @@
2.94
2.95 // run jobs
2.96 val rcs =
2.97 - for ((key, info) <- required_queue.topological_order) yield
2.98 + for ((key, info) <- queue.topological_order) yield
2.99 {
2.100 - if (list_only) { echo(key.name + " in " + info.dir); 0 }
2.101 + val name = key.name
2.102 +
2.103 + if (list_only) { echo(name + " in " + info.dir); 0 }
2.104 else {
2.105 - if (build_images) echo("Building " + key.name + " ...")
2.106 - else echo("Running " + key.name + " ...")
2.107 + val save = build_images || queue.is_inner(name)
2.108 + echo((if (save) "Building " else "Running ") + name + " ...")
2.109
2.110 - val (out, err, rc) = build_job(build_images, key.name, info).join
2.111 + val (out, err, rc) = build_job(save, name, info).join
2.112 echo_n(err)
2.113
2.114 - val log = log_dir + Path.basic(key.name)
2.115 + val log = log_dir + Path.basic(name)
2.116 if (rc == 0) {
2.117 File.write_zip(log.ext("gz"), out)
2.118 }
2.119 else {
2.120 File.write(log, out)
2.121 - echo(key.name + " FAILED")
2.122 + echo(name + " FAILED")
2.123 echo("(see also " + log.file + ")")
2.124 val lines = split_lines(out)
2.125 val tail = lines.drop(lines.length - 20 max 0)