src/Pure/General/timing.ML

--- a/src/Pure/General/timing.ML	Wed Aug 24 13:40:10 2011 +0200
+++ b/src/Pure/General/timing.ML	Wed Aug 24 15:30:43 2011 +0200
@@ -20,6 +20,7 @@
   val start: unit -> start
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
+  val is_relevant: timing -> bool
   val message: timing -> string
 end
 
@@ -67,11 +68,6 @@
 
 (* timing messages *)
 
-fun message {elapsed, cpu, gc} =
-  Time.toString elapsed ^ "s elapsed time, " ^
-  Time.toString cpu ^ "s cpu time, " ^
-  Time.toString gc ^ "s GC time" handle Time.Time => "";
-
 val min_time = Time.fromMilliseconds 1;
 
 fun is_relevant {elapsed, cpu, gc} =
@@ -79,6 +75,11 @@
   Time.>= (cpu, min_time) orelse
   Time.>= (gc, min_time);
 
+fun message {elapsed, cpu, gc} =
+  Time.toString elapsed ^ "s elapsed time, " ^
+  Time.toString cpu ^ "s cpu time, " ^
+  Time.toString gc ^ "s GC time" handle Time.Time => "";
+
 fun cond_timeit enabled msg e =
   if enabled then
     let