# HG changeset patch
# User wenzelm
# Date 1364895710 -7200
# Node ID 8e9746e584c9440a9d2a1c3cbd1ac166ebd255f6
# Parent  89bfe7a336152f869df12f10a22f74334e359922
more centralized command timing;
clarified old-style timing message;

diff -r 89bfe7a33615 -r 8e9746e584c9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 02 10:58:51 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 02 11:41:50 2013 +0200
@@ -638,32 +638,39 @@
 
 local
 
-fun timing_message tr (t: Timing.timing) =
-  (case approximative_id tr of
-    SOME id =>
-      (Output.protocol_message
-        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
-      handle Fail _ => ())
-  | NONE => ());
-
 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 timing_start = Timing.start ();
 
-      val start = Timing.start ();
-
-      val (result, status) =
+      val (result, opt_err) =
          state |>
           (apply_trans int trans
-            |> (! profiling > 0 andalso not no_timing) ? do_profiling
-            |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
-
+            |> (! profiling > 0 andalso not no_timing) ? profile (! profiling));
       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);
+      val timing_result = Timing.result timing_start;
+
+      val _ =
+        if Timing.is_relevant timing_result andalso
+          (! profiling > 0 orelse ! timing andalso not no_timing)
+        then warning (command_msg "" tr ^ ": " ^ Timing.message timing_result)
+        else ();
+      val _ =
+        if Timing.is_relevant timing_result
+        then status tr (Markup.timing timing_result)
+        else ();
+      val _ =
+        (case approximative_id tr of
+          SOME id =>
+            (Output.protocol_message
+              (Markup.command_timing ::
+                Markup.command_timing_properties id (#elapsed timing_result)) ""
+            handle Fail _ => ())
+        | NONE => ());
+    in
+      (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
+    end);
 
 in
 
diff -r 89bfe7a33615 -r 8e9746e584c9 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Apr 02 10:58:51 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Apr 02 11:41:50 2013 +0200
@@ -61,19 +61,10 @@
 
 local
 
-fun timing tr t =
-  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
-
 fun run int tr st =
   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
-    Toplevel.setmp_thread_position tr (fn () =>
-      (Goal.fork_name "Toplevel.diag" ~1
-        (fn () =>
-          let
-            val start = Timing.start ();
-            val res = Exn.interruptible_capture (fn () => Toplevel.command_exception int tr st) ();
-            val _ = timing tr (Timing.result start);
-          in Exn.release res end); ([], SOME st))) ()
+    (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
+      ([], SOME st))
   else Toplevel.command_errors int tr st;
 
 fun check_cmts tr cmts st =
@@ -106,11 +97,9 @@
 
       val _ = Multithreading.interrupted ();
       val _ = Toplevel.status tr Markup.running;
-      val start = Timing.start ();
       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
       val errs = errs1 @ errs2;
-      val _ = timing tr (Timing.result start);
       val _ = Toplevel.status tr Markup.finished;
       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     in