1.1 --- a/src/Pure/General/markup.ML	Sat Nov 06 16:03:49 2010 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Sat Nov 06 16:31:35 2010 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4    val command_spanN: string val command_span: string -> T
     1.5    val ignored_spanN: string val ignored_span: T
     1.6    val malformed_spanN: string val malformed_span: T
     1.7 +  val timing: timing -> T
     1.8    val subgoalsN: string
     1.9    val proof_stateN: string val proof_state: int -> T
    1.10    val stateN: string val state: T
    1.11 @@ -307,6 +308,10 @@
    1.12  
    1.13  (* toplevel *)
    1.14  
    1.15 +fun timing ({elapsed, cpu, gc, ...}: timing) =
    1.16 +  ("timing",
    1.17 +    [("elapsed", Time.toString elapsed), ("cpu", Time.toString cpu), ("gc", Time.toString gc)]);
    1.18 +
    1.19  val subgoalsN = "subgoals";
    1.20  val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
    1.21  

     2.1 --- a/src/Pure/ML-Systems/timing.ML	Sat Nov 06 16:03:49 2010 +0100
     2.2 +++ b/src/Pure/ML-Systems/timing.ML	Sat Nov 06 16:31:35 2010 +0100
     2.3 @@ -14,7 +14,9 @@
     2.4      val cpu_times = Timer.checkCPUTimes cpu_timer;
     2.5    in (real_timer, real_time, cpu_timer, cpu_times) end;
     2.6  
     2.7 -fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
     2.8 +type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
     2.9 +
    2.10 +fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
    2.11    let
    2.12      val real_time2 = Timer.checkRealTimer real_timer;
    2.13      val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;

     3.1 --- a/src/Pure/PIDE/document.ML	Sat Nov 06 16:03:49 2010 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Sat Nov 06 16:31:35 2010 +0100
     3.3 @@ -196,6 +196,8 @@
     3.4  
     3.5  local
     3.6  
     3.7 +fun timing tr t = Toplevel.status tr (Markup.timing t);
     3.8 +
     3.9  fun proof_status tr st =
    3.10    (case try Toplevel.proof_of st of
    3.11      SOME prf => Toplevel.status tr (Proof.status_markup prf)
    3.12 @@ -229,7 +231,9 @@
    3.13      Exn.Result () =>
    3.14        let
    3.15          val int = is_some (Toplevel.init_of tr);
    3.16 +        val start = start_timing ();
    3.17          val (errs, result) = run int tr st;
    3.18 +        val _ = timing tr (end_timing start);
    3.19          val _ = List.app (Toplevel.error_msg tr) errs;
    3.20          val _ =
    3.21            (case result of