equal
deleted
inserted
replaced
91 |
91 |
92 in |
92 in |
93 |
93 |
94 fun build args_file = Command_Line.tool (fn () => |
94 fun build args_file = Command_Line.tool (fn () => |
95 let |
95 let |
96 val (timings, (do_output, (options, (verbose, (browser_info, |
96 val (command_timings, (do_output, (options, (verbose, (browser_info, |
97 (parent_name, (name, theories))))))) = |
97 (parent_name, (name, theories))))))) = |
98 File.read (Path.explode args_file) |> YXML.parse_body |> |
98 File.read (Path.explode args_file) |> YXML.parse_body |> |
99 let open XML.Decode in |
99 let open XML.Decode in |
100 pair (list properties) (pair bool (pair Options.decode (pair bool (pair string |
100 pair (list properties) (pair bool (pair Options.decode (pair bool (pair string |
101 (pair string (pair string ((list (pair Options.decode (list string)))))))))) |
101 (pair string (pair string ((list (pair Options.decode (list string)))))))))) |
124 (false, "") "" |
124 (false, "") "" |
125 verbose; |
125 verbose; |
126 |
126 |
127 val last_timing = |
127 val last_timing = |
128 the_default Timing.zero o |
128 the_default Timing.zero o |
129 Timings.lookup (make_timings timings) o Toplevel.approximative_id; |
129 Timings.lookup (make_timings command_timings) o Toplevel.approximative_id; |
130 |
130 |
131 val res1 = |
131 val res1 = |
132 theories |> |
132 theories |> |
133 (List.app (use_theories_condition last_timing) |
133 (List.app (use_theories_condition last_timing) |
134 |> Session.with_timing name verbose |
134 |> Session.with_timing name verbose |