src/Pure/General/timing.ML

   type start
   val start: unit -> start
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
   val is_relevant: timing -> bool
+  val properties: timing -> Properties.T
   val message: timing -> string
 end
 
 structure Timing: TIMING =
 struct

     val start = start ();
     val y = f x;
   in (result start, y) end;
 
 
+(* properties *)
+
+fun property name time =
+  [(name, Time.toString time)] handle Time.Time => [];
+
+fun properties {elapsed, cpu, gc} =
+  property "time_elapsed" elapsed @
+  property "time_cpu" cpu @
+  property "time_GC" gc;
+
+
 (* timing messages *)
 
 val min_time = Time.fromMilliseconds 1;
 
 fun is_relevant {elapsed, cpu, gc} =