# 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