improved semantics of timeapp_msg

--- 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 *)