src/Pure/General/timing.ML

   include BASIC_TIMING
   type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   type start
   val start: unit -> start
   val result: start -> timing
+  val timing: ('a -> 'b) -> 'a -> timing * 'b
   val message: timing -> string
 end
 
 structure Timing: TIMING =
 struct

     val cpu = usr2 - usr + sys2 - sys + gc;
   in {elapsed = elapsed, cpu = cpu, gc = gc} end;
 
 end;
 
+fun timing f x =
+  let
+    val start = start ();
+    val y = f x;
+  in (result start, y) end;
+
 
 (* timing messages *)
 
 fun message {elapsed, cpu, gc} =
   Time.toString elapsed ^ "s elapsed time, " ^

   Time.toString gc ^ "s GC time" handle Time.Time => "";
 
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val timing_start = start ();
-      val res = Exn.capture e ();
-      val end_msg = message (result timing_start);
-      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
-    in Exn.release res end
+      val (timing, result) = timing (Exn.capture e) ();
+      val end_msg = message timing;
+      val _ =
+        if Exn.is_interrupt_exn result then ()
+        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+    in Exn.release result end
   else e ();
 
 fun timeit e = cond_timeit true "" e;
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);