# HG changeset patch
# User bulwahn
# Date 1348045064 -7200
# Node ID 0ae4216a17838121d5da761d1b1809d6bf780e2b
# Parent  4ff2976f405662738f359e6bce78aa2abca39160
recording elapsed time in mutabelle for more detailed evaluation

diff -r 4ff2976f4056 -r 0ae4216a1783 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Sep 18 14:13:58 2012 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Sep 19 10:57:44 2012 +0200
@@ -337,9 +337,9 @@
 
 fun count x = (length oo filter o equal) x
 
-fun cpu_time description e =
-  let val ({cpu, ...}, result) = Timing.timing e ()
-  in (result, (description, Time.toMilliseconds cpu)) end
+fun elapsed_time description e =
+  let val ({elapsed, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds elapsed)) end
 (*
 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
@@ -352,13 +352,13 @@
 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
-    val (res, timing) = (*cpu_time "total time"
-      (fn () => *)case try (invoke_mtd thy) t of
-          SOME (res, timing) => (res, timing)
+    val (res, timing) = elapsed_time "total time"
+      (fn () => case try (invoke_mtd thy) t of
+          SOME (res, timing) => res
         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
-           (Error, []))
+            Error))
     val _ = Output.urgent_message (" Done")
-  in (res, timing) end
+  in (res, [timing]) end
 
 (* theory -> term list -> mtd -> subentry *)
 
@@ -445,7 +445,7 @@
           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
     fun string_of_mtd_result (mtd_name, (outcome, timing)) =
       mtd_name ^ ": " ^ string_of_outcome outcome
-      (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
+      ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
       (*^ "\n" ^ string_of_reports reports*)
   in
     "mutant of " ^ thm_name ^ ":\n"