# HG changeset patch
# User haftmann
# Date 1197910670 -3600
# Node ID a089038c18932e053c04614f31608d232f9980cd
# Parent  f46ed5b333fd72a89f38fd88e6d527d648245e15
improved semantics of timeapp_msg

diff -r f46ed5b333fd -r a089038c1893 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Dec 17 17:57:48 2007 +0100
+++ b/src/Pure/General/output.ML	Mon Dec 17 17:57:50 2007 +0100
@@ -124,21 +124,26 @@
 (*global timing mode*)
 val timing = ref false;
 
-(*conditional timing*)
-fun cond_timeit flag f =
+(*generic timing combinator*)
+fun gen_timeit flag some_msg f =
   if flag then
     let
       val start = start_timing ();
       val result = f ();
-    in warning (end_timing start); result end
+      val _ = Option.map warning some_msg;
+      val _ = warning (end_timing start);
+    in result end
   else f ();
 
+(*conditional timing*)
+fun cond_timeit flag = gen_timeit flag NONE;
+
 (*unconditional timing*)
 fun timeit x = cond_timeit true x;
 
 (*timed application function*)
 fun timeap f x = timeit (fn () => f x);
-fun timeap_msg s f x = (warning s; timeap f x);
+fun timeap_msg s f x = gen_timeit true (SOME s) (fn () => f x);
 
 
 (* accumulated timing *)