support for build passing timings from Scala to ML;
authorwenzelm
Tue Feb 19 13:57:13 2013 +0100 (2013-02-19 ago)
changeset 512186425a0d3b7ac
parent 51217 65ab2c4f4c32
child 51219 2464ba6e6fc9
support for build passing timings from Scala to ML;
src/Pure/PIDE/markup.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 19 12:58:32 2013 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 13:57:13 2013 +0100
     1.3 @@ -94,6 +94,7 @@
     1.4    val gcN: string
     1.5    val timing_propertiesN: string list
     1.6    val timing_properties: Timing.timing -> Properties.T
     1.7 +  val parse_timing_properties: Properties.T -> Timing.timing
     1.8    val timingN: string val timing: Timing.timing -> T
     1.9    val subgoalsN: string
    1.10    val proof_stateN: string val proof_state: int -> T
    1.11 @@ -341,6 +342,16 @@
    1.12    (cpuN, Time.toString cpu),
    1.13    (gcN, Time.toString gc)];
    1.14  
    1.15 +fun get_time props name =
    1.16 +  (case AList.lookup (op =) props name of
    1.17 +    NONE => Time.zeroTime
    1.18 +  | SOME s => seconds (the_default 0.0 (Real.fromString s)));
    1.19 +
    1.20 +fun parse_timing_properties props =
    1.21 + {elapsed = get_time props elapsedN,
    1.22 +  cpu = get_time props cpuN,
    1.23 +  gc = get_time props gcN};
    1.24 +
    1.25  val timingN = "timing";
    1.26  fun timing t = (timingN, timing_properties t);
    1.27  
     2.1 --- a/src/Pure/Tools/build.ML	Tue Feb 19 12:58:32 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 13:57:13 2013 +0100
     2.3 @@ -80,16 +80,25 @@
     2.4            " (undefined " ^ commas conds ^ ")\n"))
     2.5    end;
     2.6  
     2.7 +structure Timings =
     2.8 +  Table(type key = Properties.T val ord = dict_ord (prod_ord fast_string_ord fast_string_ord));
     2.9 +
    2.10 +fun make_timing props =
    2.11 +  let val (t, id) = List.partition (member (op =) Markup.timing_propertiesN o fst) props
    2.12 +  in (id, Markup.parse_timing_properties t) end;
    2.13 +
    2.14 +fun make_timings timings = fold (Timings.update o make_timing) timings Timings.empty;
    2.15 +
    2.16  in
    2.17  
    2.18  fun build args_file = Command_Line.tool (fn () =>
    2.19      let
    2.20 -      val (do_output, (options, (verbose, (browser_info, (parent_name,
    2.21 -          (name, theories)))))) =
    2.22 +      val (timings, (do_output, (options, (verbose, (browser_info,
    2.23 +          (parent_name, (name, theories))))))) =
    2.24          File.read (Path.explode args_file) |> YXML.parse_body |>
    2.25            let open XML.Decode in
    2.26 -            pair bool (pair Options.decode (pair bool (pair string (pair string
    2.27 -              (pair string ((list (pair Options.decode (list string)))))))))
    2.28 +            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    2.29 +              (pair string (pair string ((list (pair Options.decode (list string))))))))))
    2.30            end;
    2.31  
    2.32        val document_variants =
    2.33 @@ -115,9 +124,13 @@
    2.34            (false, "") ""
    2.35            verbose;
    2.36  
    2.37 +      val last_timing =
    2.38 +        the_default Timing.zero o
    2.39 +          Timings.lookup (make_timings timings) o Toplevel.approximative_id;
    2.40 +
    2.41        val res1 =
    2.42          theories |>
    2.43 -          (List.app (use_theories_condition (K Timing.zero))  (* FIXME *)
    2.44 +          (List.app (use_theories_condition last_timing)
    2.45              |> Session.with_timing name verbose
    2.46              |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
    2.47              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     3.1 --- a/src/Pure/Tools/build.scala	Tue Feb 19 12:58:32 2013 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Tue Feb 19 13:57:13 2013 +0100
     3.3 @@ -443,10 +443,10 @@
     3.4        else
     3.5          {
     3.6            import XML.Encode._
     3.7 -              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
     3.8 -                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
     3.9 -              (do_output, (info.options, (verbose, (browser_info, (parent,
    3.10 -                (name, info.theories)))))))
    3.11 +              pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
    3.12 +                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    3.13 +              (Nil /* FIXME */, (do_output, (info.options, (verbose, (browser_info,
    3.14 +                (parent, (name, info.theories))))))))
    3.15          }))
    3.16  
    3.17      private val env =