--- a/src/Pure/System/build.ML Tue Jul 24 10:11:49 2012 +0200
+++ b/src/Pure/System/build.ML Tue Jul 24 10:39:03 2012 +0200
@@ -12,9 +12,8 @@
structure Build: BUILD =
struct
-fun use_theories name options =
+fun use_theories options =
Thy_Info.use_thys
- |> Session.with_timing name (Options.bool options "timing")
|> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
|> Unsynchronized.setmp print_mode
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())
@@ -27,11 +26,12 @@
fun build args_file =
let
- val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
+ val (save, (options, (timing, (verbose, (browser_info, (parent,
+ (name, (base_name, theories)))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
- pair bool (pair Options.decode (pair bool (pair string (pair string
- (pair string (pair string ((list (pair Options.decode (list string))))))))))
+ pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
+ (pair string (pair string ((list (pair Options.decode (list string)))))))))))
end;
val _ =
@@ -49,7 +49,7 @@
""
verbose;
- val _ = List.app (uncurry (use_theories name)) theories;
+ val _ = List.app (uncurry (use_theories |> Session.with_timing name timing)) theories;
val _ = Session.finish ();
val _ = if save then () else quit ();
--- a/src/Pure/System/build.scala Tue Jul 24 10:11:49 2012 +0200
+++ b/src/Pure/System/build.scala Tue Jul 24 10:39:03 2012 +0200
@@ -342,7 +342,7 @@
}
private def start_job(name: String, info: Session.Info, output: Option[String],
- options: Options, verbose: Boolean, browser_info: Path): Job =
+ options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
{
val parent = info.parent.getOrElse("")
@@ -373,10 +373,10 @@
val args_xml =
{
import XML.Encode._
- pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
- pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
- (output.isDefined, (options, (verbose, (browser_info, (parent,
- (name, (info.base_name, info.theories))))))))
+ 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.isDefined, (options, (timing, (verbose, (browser_info, (parent,
+ (name, (info.base_name, info.theories)))))))))
}
new Job(cwd, env, script, YXML.string_of_body(args_xml))
}
@@ -388,7 +388,7 @@
private def sleep(): Unit = Thread.sleep(500)
def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
- list_only: Boolean, system_mode: Boolean, verbose: Boolean,
+ list_only: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
{
val options = (Options.init() /: more_options)(_.define_simple(_))
@@ -458,7 +458,7 @@
Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
else None
echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
- val job = start_job(name, info, output, options, verbose, browser_info)
+ val job = start_job(name, info, output, options, timing, verbose, browser_info)
loop(pending, running + (name -> job), results)
}
else {
@@ -487,9 +487,10 @@
Properties.Value.Int(max_jobs) ::
Properties.Value.Boolean(list_only) ::
Properties.Value.Boolean(system_mode) ::
+ Properties.Value.Boolean(timing) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(more_dirs, options, sessions) =>
- build(all_sessions, build_images, max_jobs, list_only, system_mode,
+ build(all_sessions, build_images, max_jobs, list_only, system_mode, timing,
verbose, more_dirs.map(Path.explode), options, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}