timing is command line options, not system option;

--- a/etc/options	Tue Jul 24 10:11:49 2012 +0200
+++ b/etc/options	Tue Jul 24 10:39:03 2012 +0200
@@ -18,7 +18,5 @@
 declare proofs : int = 0
 declare quick_and_dirty : bool = false
 
-declare timing : bool = false
-
 declare condition : string = ""
 

--- a/lib/Tools/build	Tue Jul 24 10:11:49 2012 +0200
+++ b/lib/Tools/build	Tue Jul 24 10:39:03 2012 +0200
@@ -22,6 +22,7 @@
   echo "    -l           list sessions 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"
@@ -54,12 +55,13 @@
 MAX_JOBS=1
 LIST_ONLY=false
 SYSTEM_MODE=false
+TIMING=false
 VERBOSE=false
 
 declare -a MORE_DIRS=()
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 
-while getopts "abd:j:lo:sv" OPT
+while getopts "abd:j:lo:stv" OPT
 do
   case "$OPT" in
     a)
@@ -84,6 +86,9 @@
     s)
       SYSTEM_MODE="true"
       ;;
+    t)
+      TIMING="true"
+      ;;
     v)
       VERBOSE="true"
       ;;
@@ -101,5 +106,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 exec "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
-  "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$TIMING" \
+  "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"

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