1.1 --- a/src/Pure/General/timing.ML	Wed Apr 03 21:30:32 2013 +0200
     1.2 +++ b/src/Pure/General/timing.ML	Wed Apr 03 21:48:43 2013 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val is_relevant_time: Time.time -> bool
     1.5    val is_relevant: timing -> bool
     1.6    val message: timing -> string
     1.7 +  val status: ('a -> 'b) -> 'a -> 'b
     1.8  end
     1.9  
    1.10  structure Timing: TIMING =
    1.11 @@ -89,10 +90,10 @@
    1.12  fun cond_timeit enabled msg e =
    1.13    if enabled then
    1.14      let
    1.15 -      val (timing, result) = timing (Exn.interruptible_capture e) ();
    1.16 +      val (t, result) = timing (Exn.interruptible_capture e) ();
    1.17        val _ =
    1.18 -        if is_relevant timing then
    1.19 -          let val end_msg = message timing
    1.20 +        if is_relevant t then
    1.21 +          let val end_msg = message t
    1.22            in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
    1.23          else ();
    1.24      in Exn.release result end
    1.25 @@ -102,6 +103,12 @@
    1.26  fun timeap f x = timeit (fn () => f x);
    1.27  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
    1.28  
    1.29 +fun status f x =
    1.30 +  let
    1.31 +    val (t, result) = timing (Exn.interruptible_capture f) x;
    1.32 +    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
    1.33 +  in Exn.release result end;
    1.34 +
    1.35  end;
    1.36  
    1.37  structure Basic_Timing: BASIC_TIMING = Timing;

     2.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 03 21:30:32 2013 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 03 21:48:43 2013 +0200
     2.3 @@ -1163,7 +1163,7 @@
     2.4      state |> future_proof (fn state' =>
     2.5        Goal.fork_params
     2.6          {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
     2.7 -        (fn () => ((), proof2 state'))) |> snd |> done
     2.8 +        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
     2.9    else proof1 state;
    2.10  
    2.11  in

     3.1 --- a/src/Pure/PIDE/markup.ML	Wed Apr 03 21:30:32 2013 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Wed Apr 03 21:48:43 2013 +0200
     3.3 @@ -94,14 +94,14 @@
     3.4    val cpuN: string
     3.5    val gcN: string
     3.6    val timing_propertiesN: string list
     3.7 -  val timing_properties: Timing.timing -> Properties.T
     3.8 -  val parse_timing_properties: Properties.T -> Timing.timing
     3.9 +  val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
    3.10 +  val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
    3.11    val command_timingN: string
    3.12    val command_timing_properties:
    3.13      {file: string, offset: int, name: string} -> Time.time -> Properties.T
    3.14    val parse_command_timing_properties:
    3.15      Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
    3.16 -  val timingN: string val timing: Timing.timing -> T
    3.17 +  val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
    3.18    val subgoalsN: string
    3.19    val proof_stateN: string val proof_state: int -> T
    3.20    val stateN: string val state: T

     4.1 --- a/src/Pure/ROOT.ML	Wed Apr 03 21:30:32 2013 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Wed Apr 03 21:48:43 2013 +0200
     4.3 @@ -28,9 +28,9 @@
     4.4  
     4.5  use "General/properties.ML";
     4.6  use "General/output.ML";
     4.7 -use "General/timing.ML";
     4.8  use "PIDE/markup.ML";
     4.9  fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
    4.10 +use "General/timing.ML";
    4.11  use "General/scan.ML";
    4.12  use "General/source.ML";
    4.13  use "General/symbol.ML";