# HG changeset patch
# User wenzelm
# Date 1011297571 -3600
# Node ID fc716621f19d5419e515e387a10cb548cfe70e99
# Parent  c992ee4168ff30042cda01db4dd10f6a4ee51f08
added timeap_msg;

diff -r c992ee4168ff -r fc716621f19d src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jan 17 19:37:57 2002 +0100
+++ b/src/Pure/library.ML	Thu Jan 17 20:59:31 2002 +0100
@@ -270,6 +270,7 @@
   val cond_timeit: bool -> (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
 
   (*misc*)
@@ -1235,6 +1236,7 @@
 
 (*timed application function*)
 fun timeap f x = timeit (fn () => f x);
+fun timeap_msg s f x = (warning s; timeap f x);
 
 (*global timing mode*)
 val timing = ref false;