# 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))
       }
     }