# HG changeset patch
# User wenzelm
# Date 1197930780 -3600
# Node ID bfa774974b6c753a9ac3aa29776aaeca2455a91d
# Parent  c36e10812ae4a4822d9882b2c2bdc8d3429871b0
cond_timeit: added message argument, use Exn.capture/release;
tuned;

diff -r c36e10812ae4 -r bfa774974b6c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Dec 17 23:26:27 2007 +0100
+++ b/src/Pure/General/output.ML	Mon Dec 17 23:33:00 2007 +0100
@@ -14,11 +14,11 @@
   val warning: string -> unit
   val tolerate_legacy_features: bool ref
   val legacy_feature: string -> unit
-  val timing: bool ref
-  val cond_timeit: bool -> (unit -> 'a) -> 'a
+  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
   val timeit: (unit -> 'a) -> 'a
   val timeap: ('a -> 'b) -> 'a -> 'b
   val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
+  val timing: bool ref
   val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
 end;
 
@@ -121,31 +121,27 @@
 
 (** timing **)
 
-(*global timing mode*)
-val timing = ref false;
-
-(*generic timing combinator*)
-fun gen_timeit flag msg f =
+(*conditional timing with message*)
+fun cond_timeit flag msg e =
   if flag then
     let
       val start = start_timing ();
-      val result = f ();
+      val result = Exn.capture e ();
       val end_msg = end_timing start;
-      val output_msg = if msg = "" then end_msg
-        else msg ^ " - " ^ end_msg;
-      val _ = warning output_msg;
-    in result end
-  else f ();
-
-(*conditional timing*)
-fun cond_timeit flag = gen_timeit flag "";
+      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+    in Exn.release result end
+  else e ();
 
 (*unconditional timing*)
-fun timeit x = cond_timeit true x;
+fun timeit e = cond_timeit true "" e;
 
 (*timed application function*)
 fun timeap f x = timeit (fn () => f x);
-fun timeap_msg s f x = gen_timeit true s (fn () => f x);
+fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
+
+
+(*global timing mode*)
+val timing = ref false;
 
 
 (* accumulated timing *)