# HG changeset patch # User wenzelm # Date 1361278633 -3600 # Node ID 6425a0d3b7ac11e71d385308fd5966fb9d1ed1b8 # Parent 65ab2c4f4c32ff0962f318ac7f73a56f0d6ed885 support for build passing timings from Scala to ML; diff -r 65ab2c4f4c32 -r 6425a0d3b7ac src/Pure/PIDE/markup.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); diff -r 65ab2c4f4c32 -r 6425a0d3b7ac src/Pure/Tools/build.ML --- 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") diff -r 65ab2c4f4c32 -r 6425a0d3b7ac src/Pure/Tools/build.scala --- 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 =