# HG changeset patch # User wenzelm # Date 1343387712 -7200 # Node ID c168bc64f2a84c8034fa67d1ebe1ec41de13dbd4 # Parent 8c26657e73c3b857d4d502229d7a9166c6a65e5e fewer options; diff -r 8c26657e73c3 -r c168bc64f2a8 lib/Tools/build --- a/lib/Tools/build Fri Jul 27 13:08:46 2012 +0200 +++ b/lib/Tools/build Fri Jul 27 13:15:12 2012 +0200 @@ -34,7 +34,6 @@ echo " -n no build -- test dependencies only" echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" echo " -s system build mode: produce output in ISABELLE_HOME" - echo " -t inner session timing" echo " -v verbose" echo echo " Build and manage Isabelle sessions, depending on implicit" @@ -65,10 +64,9 @@ NO_BUILD=false eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" SYSTEM_MODE=false -TIMING=false VERBOSE=false -while getopts "abd:g:j:no:stv" OPT +while getopts "abd:g:j:no:sv" OPT do case "$OPT" in a) @@ -96,9 +94,6 @@ s) SYSTEM_MODE="true" ;; - t) - TIMING="true" - ;; v) VERBOSE="true" ;; @@ -126,7 +121,7 @@ fi "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ + "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?" diff -r 8c26657e73c3 -r c168bc64f2a8 src/Pure/System/build.ML --- a/src/Pure/System/build.ML Fri Jul 27 13:08:46 2012 +0200 +++ b/src/Pure/System/build.ML Fri Jul 27 13:15:12 2012 +0200 @@ -56,12 +56,12 @@ fun build args_file = let - val (do_output, (options, (timing, (verbose, (browser_info, (parent_name, - (name, theories))))))) = + val (do_output, (options, (verbose, (browser_info, (parent_name, + (name, theories)))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in - pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string - (pair string ((list (pair Options.decode (list string)))))))))) + pair bool (pair Options.decode (pair bool (pair string (pair string + (pair string ((list (pair Options.decode (list string))))))))) end; val _ = @@ -74,7 +74,7 @@ (Options.string options "document_dump", Present.dump_mode (Options.string options "document_dump_mode")) "" verbose; - val _ = Session.with_timing name timing (List.app use_theories) theories; + val _ = Session.with_timing name verbose (List.app use_theories) theories; val _ = Session.finish (); val _ = if do_output then () else quit (); in () end diff -r 8c26657e73c3 -r c168bc64f2a8 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Fri Jul 27 13:08:46 2012 +0200 +++ b/src/Pure/System/build.scala Fri Jul 27 13:15:12 2012 +0200 @@ -334,7 +334,7 @@ } private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean, - options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = + options: Options, verbose: Boolean, browser_info: Path): Job = { // global browser info dir if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) @@ -385,10 +385,10 @@ val args_xml = { import XML.Encode._ - pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, - pair(string, list(pair(Options.encode, list(Path.encode))))))))))( - (do_output, (options, (timing, (verbose, (browser_info, (parent, - (name, info.theories)))))))) + pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string, + pair(string, list(pair(Options.encode, list(Path.encode)))))))))( + (do_output, (options, (verbose, (browser_info, (parent, + (name, info.theories))))))) } new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output) } @@ -441,7 +441,6 @@ no_build: Boolean = false, build_options: List[String] = Nil, system_mode: Boolean = false, - timing: Boolean = false, verbose: Boolean = false, sessions: List[String] = Nil): Int = { @@ -526,7 +525,7 @@ else if (parent_ok) { echo((if (do_output) "Building " else "Running ") + name + " ...") val job = - start_job(name, info, output, do_output, info.options, timing, verbose, browser_info) + start_job(name, info, output, do_output, info.options, verbose, browser_info) loop(pending, running + (name -> job), results) } else { @@ -561,11 +560,10 @@ 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_heap, more_dirs.map(Path.explode), session_groups, - max_jobs, no_build, build_options, system_mode, timing, verbose, sessions) + max_jobs, no_build, build_options, system_mode, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } }