support for build passing timings from Scala to ML;

--- a/src/Pure/PIDE/markup.ML	Tue Feb 19 12:58:32 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 13:57:13 2013 +0100
@@ -94,6 +94,7 @@
   val gcN: string
   val timing_propertiesN: string list
   val timing_properties: Timing.timing -> Properties.T
+  val parse_timing_properties: Properties.T -> Timing.timing
   val timingN: string val timing: Timing.timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
@@ -341,6 +342,16 @@
   (cpuN, Time.toString cpu),
   (gcN, Time.toString gc)];
 
+fun get_time props name =
+  (case AList.lookup (op =) props name of
+    NONE => Time.zeroTime
+  | SOME s => seconds (the_default 0.0 (Real.fromString s)));
+
+fun parse_timing_properties props =
+ {elapsed = get_time props elapsedN,
+  cpu = get_time props cpuN,
+  gc = get_time props gcN};
+
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 

--- a/src/Pure/Tools/build.ML	Tue Feb 19 12:58:32 2013 +0100
+++ b/src/Pure/Tools/build.ML	Tue Feb 19 13:57:13 2013 +0100
@@ -80,16 +80,25 @@
           " (undefined " ^ commas conds ^ ")\n"))
   end;
 
+structure Timings =
+  Table(type key = Properties.T val ord = dict_ord (prod_ord fast_string_ord fast_string_ord));
+
+fun make_timing props =
+  let val (t, id) = List.partition (member (op =) Markup.timing_propertiesN o fst) props
+  in (id, Markup.parse_timing_properties t) end;
+
+fun make_timings timings = fold (Timings.update o make_timing) timings Timings.empty;
+
 in
 
 fun build args_file = Command_Line.tool (fn () =>
     let
-      val (do_output, (options, (verbose, (browser_info, (parent_name,
-          (name, theories)))))) =
+      val (timings, (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 string (pair string
-              (pair string ((list (pair Options.decode (list string)))))))))
+            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
+              (pair string (pair string ((list (pair Options.decode (list string))))))))))
           end;
 
       val document_variants =
@@ -115,9 +124,13 @@
           (false, "") ""
           verbose;
 
+      val last_timing =
+        the_default Timing.zero o
+          Timings.lookup (make_timings timings) o Toplevel.approximative_id;
+
       val res1 =
         theories |>
-          (List.app (use_theories_condition (K Timing.zero))  (* FIXME *)
+          (List.app (use_theories_condition last_timing)
             |> Session.with_timing name verbose
             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")

--- a/src/Pure/Tools/build.scala	Tue Feb 19 12:58:32 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Feb 19 13:57:13 2013 +0100
@@ -443,10 +443,10 @@
       else
         {
           import XML.Encode._
-              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
-                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
-              (do_output, (info.options, (verbose, (browser_info, (parent,
-                (name, info.theories)))))))
+              pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
+                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+              (Nil /* FIXME */, (do_output, (info.options, (verbose, (browser_info,
+                (parent, (name, info.theories))))))))
         }))
 
     private val env =