timing status for forked diagnostic commands;
authorwenzelm
Sat Mar 30 16:34:02 2013 +0100 (2013-03-30 ago)
changeset 515898ea0a5dd5a35
parent 51588 167e2d64327a
child 51590 c52891242de2
timing status for forked diagnostic commands;
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Sat Mar 30 16:16:24 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Mar 30 16:34:02 2013 +0100
     1.3 @@ -61,11 +61,19 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun timing tr t =
     1.8 +  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
     1.9 +
    1.10  fun run int tr st =
    1.11    if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    1.12      Toplevel.setmp_thread_position tr (fn () =>
    1.13        (Goal.fork_name "Toplevel.diag" ~1
    1.14 -        (fn () => Toplevel.command_exception int tr st); ([], SOME st))) ()
    1.15 +        (fn () =>
    1.16 +          let
    1.17 +            val start = Timing.start ();
    1.18 +            val res = Exn.interruptible_capture (fn () => Toplevel.command_exception int tr st) ();
    1.19 +            val _ = timing tr (Timing.result start);
    1.20 +          in Exn.release res end); ([], SOME st))) ()
    1.21    else Toplevel.command_errors int tr st;
    1.22  
    1.23  fun check_cmts tr cmts st =
    1.24 @@ -75,9 +83,6 @@
    1.25          (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    1.26            handle exn => ML_Compiler.exn_messages_ids exn)) ();
    1.27  
    1.28 -fun timing tr t =
    1.29 -  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
    1.30 -
    1.31  fun proof_status tr st =
    1.32    (case try Toplevel.proof_of st of
    1.33      SOME prf => Toplevel.status tr (Proof.status_markup prf)