# HG changeset patch
# User wenzelm
# Date 1300655292 -3600
# Node ID 75417ef605ba3aa6a02235da2bf256e70a0519b6
# Parent  1694cc477045a27e9aa0967c0dc98bd739f106b4
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);

diff -r 1694cc477045 -r 75417ef605ba src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 21:44:38 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 22:08:12 2011 +0100
@@ -209,11 +209,8 @@
   | SOME NONE => error ("bad option: " ^ key)
   | NONE => default)
 
-fun cpu_time f x =  (* FIXME !? *)
-  let
-    val start = Timing.start ()
-    val result = Exn.capture (fn () => f x) ()
-    val time = Time.toMilliseconds (#cpu (Timing.result start))
-  in (Exn.release result, time) end
+fun cpu_time f x =
+  let val ({cpu, ...}, y) = Timing.timing f x
+  in (y, Time.toMilliseconds cpu) end
 
 end
diff -r 1694cc477045 -r 75417ef605ba src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 21:44:38 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 22:08:12 2011 +0100
@@ -332,12 +332,9 @@
 
 fun count x = (length oo filter o equal) x
 
-fun cpu_time description f =  (* FIXME !? *)
-  let
-    val start = Timing.start ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (Timing.result start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 (*
 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
diff -r 1694cc477045 -r 75417ef605ba src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 21:44:38 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 22:08:12 2011 +0100
@@ -211,12 +211,9 @@
 
 val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
-fun cpu_time description f =  (* FIXME !? *)
-  let
-    val start = Timing.start ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (Timing.result start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 
 fun compile_term compilation options ctxt t =
   let
diff -r 1694cc477045 -r 75417ef605ba src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Mar 20 21:44:38 2011 +0100
+++ b/src/Tools/quickcheck.ML	Sun Mar 20 22:08:12 2011 +0100
@@ -167,12 +167,9 @@
     val frees = Term.add_frees t [];
   in (frees, list_abs_free (frees, t)) end
 
-fun cpu_time description f =  (* FIXME !? *)
-  let
-    val start = Timing.start ()
-    val result = Exn.capture f ()
-    val time = Time.toMilliseconds (#cpu (Timing.result start))
-  in (Exn.release result, (description, time)) end
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
 
 fun limit ctxt (limit_time, is_interactive) f exc () =
   if limit_time then