--- a/src/Pure/Isar/toplevel.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Feb 19 10:55:11 2013 +0100
@@ -612,12 +612,22 @@
local
+fun timing_message tr t =
+ if Timing.is_relevant t then
+ Output.protocol_message
+ (Markup.command_timing :: (Markup.nameN, name_of tr) ::
+ Position.properties_of (pos_of tr) @ Markup.timing_properties t) ""
+ handle Fail _ => ()
+ else ();
+
fun app int (tr as Transition {trans, print, no_timing, ...}) =
setmp_thread_position tr (fn state =>
let
fun do_timing f x = (warning (command_msg "" tr); timeap f x);
fun do_profiling f x = profile (! profiling) f x;
+ val start = Timing.start ();
+
val (result, status) =
state |>
(apply_trans int trans
@@ -625,6 +635,8 @@
|> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
+
+ val _ = timing_message tr (Timing.result start);
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
in
--- a/src/Pure/PIDE/markup.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Feb 19 10:55:11 2013 +0100
@@ -135,6 +135,7 @@
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
val task_statistics: Properties.entry
+ val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
@@ -415,6 +416,8 @@
val task_statistics = (functionN, "task_statistics");
+val command_timing = (functionN, "command_timing");
+
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
--- a/src/Pure/Tools/build.ML Mon Feb 18 18:34:55 2013 +0100
+++ b/src/Pure/Tools/build.ML Tue Feb 19 10:55:11 2013 +0100
@@ -16,30 +16,23 @@
local
-fun ML_statistics (function :: stats) "" =
- if function = Markup.ML_statistics then SOME stats
- else NONE
- | ML_statistics _ _ = NONE;
+(* FIXME avoid hardwired stuff!? *)
+val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
-fun task_statistics (function :: stats) "" =
- if function = Markup.task_statistics then SOME stats
- else NONE
- | task_statistics _ _ = NONE;
-
-val print_properties = YXML.string_of_body o XML.Encode.properties;
+fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
in
fun protocol_message props output =
- (case ML_statistics props output of
- SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
- | NONE =>
- (case task_statistics props output of
- SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
- | NONE =>
- (case Markup.dest_loading_theory props of
- SOME name => writeln ("\floading_theory = " ^ name)
- | NONE => raise Fail "Undefined Output.protocol_message")));
+ (case props of
+ function :: args =>
+ if member (op =) protocol_echo function then
+ writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+ else
+ (case Markup.dest_loading_theory props of
+ SOME name => writeln ("\floading_theory = " ^ name)
+ | NONE => protocol_undef ())
+ | [] => protocol_undef ());
end;