# HG changeset patch
# User wenzelm
# Date 1364657642 -3600
# Node ID 8ea0a5dd5a35b1d675b5d4970e52eb5001fa3d9a
# Parent  167e2d64327a3dfd40ba484fedbf9449a68b17d1
timing status for forked diagnostic commands;

diff -r 167e2d64327a -r 8ea0a5dd5a35 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Mar 30 16:16:24 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Sat Mar 30 16:34:02 2013 +0100
@@ -61,11 +61,19 @@
 
 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 () => Toplevel.command_exception int tr st); ([], SOME st))) ()
+        (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))) ()
   else Toplevel.command_errors int tr st;
 
 fun check_cmts tr cmts st =
@@ -75,9 +83,6 @@
         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
           handle exn => ML_Compiler.exn_messages_ids exn)) ();
 
-fun timing tr t =
-  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
-
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
     SOME prf => Toplevel.status tr (Proof.status_markup prf)