src/Pure/Tools/build.ML
changeset 51218 6425a0d3b7ac
parent 51217 65ab2c4f4c32
child 51220 e140c8fa485a
     1.1 --- a/src/Pure/Tools/build.ML	Tue Feb 19 12:58:32 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 13:57:13 2013 +0100
     1.3 @@ -80,16 +80,25 @@
     1.4            " (undefined " ^ commas conds ^ ")\n"))
     1.5    end;
     1.6  
     1.7 +structure Timings =
     1.8 +  Table(type key = Properties.T val ord = dict_ord (prod_ord fast_string_ord fast_string_ord));
     1.9 +
    1.10 +fun make_timing props =
    1.11 +  let val (t, id) = List.partition (member (op =) Markup.timing_propertiesN o fst) props
    1.12 +  in (id, Markup.parse_timing_properties t) end;
    1.13 +
    1.14 +fun make_timings timings = fold (Timings.update o make_timing) timings Timings.empty;
    1.15 +
    1.16  in
    1.17  
    1.18  fun build args_file = Command_Line.tool (fn () =>
    1.19      let
    1.20 -      val (do_output, (options, (verbose, (browser_info, (parent_name,
    1.21 -          (name, theories)))))) =
    1.22 +      val (timings, (do_output, (options, (verbose, (browser_info,
    1.23 +          (parent_name, (name, theories))))))) =
    1.24          File.read (Path.explode args_file) |> YXML.parse_body |>
    1.25            let open XML.Decode in
    1.26 -            pair bool (pair Options.decode (pair bool (pair string (pair string
    1.27 -              (pair string ((list (pair Options.decode (list string)))))))))
    1.28 +            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    1.29 +              (pair string (pair string ((list (pair Options.decode (list string))))))))))
    1.30            end;
    1.31  
    1.32        val document_variants =
    1.33 @@ -115,9 +124,13 @@
    1.34            (false, "") ""
    1.35            verbose;
    1.36  
    1.37 +      val last_timing =
    1.38 +        the_default Timing.zero o
    1.39 +          Timings.lookup (make_timings timings) o Toplevel.approximative_id;
    1.40 +
    1.41        val res1 =
    1.42          theories |>
    1.43 -          (List.app (use_theories_condition (K Timing.zero))  (* FIXME *)
    1.44 +          (List.app (use_theories_condition last_timing)
    1.45              |> Session.with_timing name verbose
    1.46              |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
    1.47              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")