--- 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;