explicit "timing" status for toplevel transactions;

--- a/src/Pure/General/markup.ML	Sat Nov 06 16:03:49 2010 +0100
+++ b/src/Pure/General/markup.ML	Sat Nov 06 16:31:35 2010 +0100
@@ -99,6 +99,7 @@
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
+  val timing: timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
@@ -307,6 +308,10 @@
 
 (* toplevel *)
 
+fun timing ({elapsed, cpu, gc, ...}: timing) =
+  ("timing",
+    [("elapsed", Time.toString elapsed), ("cpu", Time.toString cpu), ("gc", Time.toString gc)]);
+
 val subgoalsN = "subgoals";
 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
 

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

--- a/src/Pure/PIDE/document.ML	Sat Nov 06 16:03:49 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Sat Nov 06 16:31:35 2010 +0100
@@ -196,6 +196,8 @@
 
 local
 
+fun timing tr t = Toplevel.status tr (Markup.timing t);
+
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
     SOME prf => Toplevel.status tr (Proof.status_markup prf)
@@ -229,7 +231,9 @@
     Exn.Result () =>
       let
         val int = is_some (Toplevel.init_of tr);
+        val start = start_timing ();
         val (errs, result) = run int tr st;
+        val _ = timing tr (end_timing start);
         val _ = List.app (Toplevel.error_msg tr) errs;
         val _ =
           (case result of