--- a/src/Pure/System/build.ML Thu Jul 26 12:32:25 2012 +0200
+++ b/src/Pure/System/build.ML Thu Jul 26 12:59:09 2012 +0200
@@ -50,7 +50,7 @@
fun build args_file =
let
- val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
+ val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
(name, (base_name, theories)))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
@@ -59,7 +59,7 @@
end;
val _ =
- Session.init save false
+ Session.init do_output false
(Options.bool options "browser_info") browser_info
(Options.string options "document")
(Options.bool options "document_graph")
@@ -70,7 +70,7 @@
verbose;
val _ = Session.with_timing name timing (List.app use_theories) theories;
val _ = Session.finish ();
- val _ = if save then () else quit ();
+ val _ = if do_output then () else quit ();
in () end
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
--- a/src/Pure/System/build.scala Thu Jul 26 12:32:25 2012 +0200
+++ b/src/Pure/System/build.scala Thu Jul 26 12:59:09 2012 +0200
@@ -320,7 +320,7 @@
/* jobs */
private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
- val output_path: Option[Path])
+ output: Path, do_output: Boolean)
{
private val args_file = File.tmp_file("args")
private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
@@ -332,9 +332,10 @@
def terminate: Unit = thread.interrupt
def is_finished: Boolean = result.is_finished
def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
+ def output_path: Option[Path] = if (do_output) Some(output) else None
}
- private def start_job(name: String, info: Session.Info, output_path: Option[Path],
+ private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
{
// global browser info dir
@@ -352,21 +353,26 @@
val parent = info.parent.getOrElse("")
val parent_base_name = info.parent_base_name.getOrElse("")
- val output =
- output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" }
-
val cwd = info.dir.file
- val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output)
+ val env =
+ Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
val script =
- if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
+ if (is_pure(name)) {
+ if (do_output) "./build " + name + " \"$OUTPUT\""
+ else """ rm -f "$OUTPUT"; ./build """ + name
+ }
else {
"""
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
""" +
- (if (output_path.isDefined)
- """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
+ (if (do_output)
+ """
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
+ """
else
- """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
+ """
+ rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
+ """) +
"""
RC="$?"
@@ -384,10 +390,10 @@
import XML.Encode._
pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
- (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
+ (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
(name, (info.base_name, info.theories)))))))))
}
- new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path)
+ new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
}
@@ -431,7 +437,7 @@
def build(
all_sessions: Boolean = false,
- build_images: Boolean = false,
+ build_heap: Boolean = false,
more_dirs: List[Path] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
@@ -496,17 +502,15 @@
{ // check/start next job
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
- val output =
- if (build_images || queue.is_inner(name))
- Some(output_dir + Path.basic(name))
- else None
+ val output = output_dir + Path.basic(name)
+ val do_output = build_heap || queue.is_inner(name)
val current =
{
input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
case Some(dir) =>
check_stamps(dir, name) match {
- case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty)
+ case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
case None => false
}
case None => false
@@ -515,8 +519,9 @@
if (current || no_build)
loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
else if (info.parent.map(results(_)).forall(_ == 0)) {
- echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
- val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
+ echo((if (do_output) "Building " else "Running ") + name + " ...")
+ val job =
+ start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)
loop(pending, running + (name -> job), results)
}
else {
@@ -547,14 +552,14 @@
args.toList match {
case
Properties.Value.Boolean(all_sessions) ::
- Properties.Value.Boolean(build_images) ::
+ Properties.Value.Boolean(build_heap) ::
Properties.Value.Int(max_jobs) ::
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(timing) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
- build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
+ build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}