structure Timing: covers former start_timing/end_timing and Output.timeit etc;
authorwenzelm
Sun Mar 20 21:28:11 2011 +0100 (2011-03-20)
changeset 420122c3fe3cbebae
parent 42011 dee23d63d466
child 42013 1694cc477045
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
src/HOL/Matrix/Compute_Oracle/report.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/ex/SAT_Examples.thy
src/Provers/blast.ML
src/Pure/General/markup.ML
src/Pure/General/output.ML
src/Pure/General/timing.ML
src/Pure/IsaMakefile
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/PIDE/document.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ROOT.ML
src/Pure/System/session.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:20:07 2011 +0100
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/report.ML	Sun Mar 20 21:28:11 2011 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4  
     1.5  fun timeit f =
     1.6      let
     1.7 -        val t1 = start_timing ()
     1.8 +        val t1 = Timing.start ()
     1.9          val x = f ()
    1.10 -        val t2 = #message (end_timing t1)
    1.11 +        val t2 = Timing.message (Timing.result t1)
    1.12          val _ = writeln ((report_space ()) ^ "--> "^t2)
    1.13      in
    1.14          x       
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 21:20:07 2011 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 21:28:11 2011 +0100
     2.3 @@ -209,11 +209,11 @@
     2.4    | SOME NONE => error ("bad option: " ^ key)
     2.5    | NONE => default)
     2.6  
     2.7 -fun cpu_time f x =
     2.8 +fun cpu_time f x =  (* FIXME !? *)
     2.9    let
    2.10 -    val start = start_timing ()
    2.11 +    val start = Timing.start ()
    2.12      val result = Exn.capture (fn () => f x) ()
    2.13 -    val time = Time.toMilliseconds (#cpu (end_timing start))
    2.14 +    val time = Time.toMilliseconds (#cpu (Timing.result start))
    2.15    in (Exn.release result, time) end
    2.16  
    2.17  end
     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 21:20:07 2011 +0100
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 21:28:11 2011 +0100
     3.3 @@ -332,11 +332,11 @@
     3.4  
     3.5  fun count x = (length oo filter o equal) x
     3.6  
     3.7 -fun cpu_time description f =
     3.8 +fun cpu_time description f =  (* FIXME !? *)
     3.9    let
    3.10 -    val start = start_timing ()
    3.11 +    val start = Timing.start ()
    3.12      val result = Exn.capture f ()
    3.13 -    val time = Time.toMilliseconds (#cpu (end_timing start))
    3.14 +    val time = Time.toMilliseconds (#cpu (Timing.result start))
    3.15    in (Exn.release result, (description, time)) end
    3.16  (*
    3.17  fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 21:20:07 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 21:28:11 2011 +0100
     4.3 @@ -211,11 +211,11 @@
     4.4  
     4.5  val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
     4.6  
     4.7 -fun cpu_time description f =
     4.8 +fun cpu_time description f =  (* FIXME !? *)
     4.9    let
    4.10 -    val start = start_timing ()
    4.11 +    val start = Timing.start ()
    4.12      val result = Exn.capture f ()
    4.13 -    val time = Time.toMilliseconds (#cpu (end_timing start))
    4.14 +    val time = Time.toMilliseconds (#cpu (Timing.result start))
    4.15    in (Exn.release result, (description, time)) end
    4.16  
    4.17  fun compile_term compilation options ctxt t =
     5.1 --- a/src/HOL/ex/SAT_Examples.thy	Sun Mar 20 21:20:07 2011 +0100
     5.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sun Mar 20 21:28:11 2011 +0100
     5.3 @@ -536,13 +536,12 @@
     5.4    fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
     5.5      | and_to_list fm acc = rev (fm :: acc)
     5.6    val clauses = and_to_list prop_fm []
     5.7 -  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
     5.8 -    clauses
     5.9 -  val cterms  = map (Thm.cterm_of @{theory}) terms
    5.10 -  val timer   = start_timing ()
    5.11 -  val thm     = sat.rawsat_thm @{context} cterms
    5.12 +  val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
    5.13 +  val cterms = map (Thm.cterm_of @{theory}) terms
    5.14 +  val start = Timing.start ()
    5.15 +  val thm = sat.rawsat_thm @{context} cterms
    5.16  in
    5.17 -  (end_timing timer, !sat.counter)
    5.18 +  (Timing.result start, ! sat.counter)
    5.19  end;
    5.20  *}
    5.21  
     6.1 --- a/src/Provers/blast.ML	Sun Mar 20 21:20:07 2011 +0100
     6.2 +++ b/src/Provers/blast.ML	Sun Mar 20 21:28:11 2011 +0100
     6.3 @@ -914,7 +914,7 @@
     6.4  
     6.5  fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
     6.6    if b then
     6.7 -    writeln (#message (end_timing start) ^ " for search.  Closed: "
     6.8 +    writeln (Timing.message (Timing.result start) ^ " for search.  Closed: "
     6.9               ^ string_of_int (!nclosed) ^
    6.10               " tried: " ^ string_of_int (!ntried) ^
    6.11               " tactics: " ^ string_of_int (length tacs))
    6.12 @@ -1256,7 +1256,7 @@
    6.13        val hyps  = strip_imp_prems skoprem
    6.14        and concl = strip_imp_concl skoprem
    6.15        fun cont (tacs,_,choices) =
    6.16 -          let val start = start_timing ()
    6.17 +          let val start = Timing.start ()
    6.18            in
    6.19            case Seq.pull(EVERY' (rev tacs) i st) of
    6.20                NONE => (writeln ("PROOF FAILED for depth " ^
    6.21 @@ -1265,7 +1265,7 @@
    6.22                         else ();
    6.23                         backtrack choices)
    6.24              | cell => (if (!trace orelse !stats)
    6.25 -                       then writeln (#message (end_timing start) ^ " for reconstruction")
    6.26 +                       then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
    6.27                         else ();
    6.28                         Seq.make(fn()=> cell))
    6.29            end
    6.30 @@ -1273,13 +1273,13 @@
    6.31    handle PROVE     => Seq.empty
    6.32  
    6.33  (*Public version with fixed depth*)
    6.34 -fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
    6.35 +fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
    6.36  
    6.37  val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
    6.38  
    6.39  fun blast_tac cs i st =
    6.40      ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
    6.41 -        (timing_depth_tac (start_timing ()) cs) 0) i
    6.42 +        (timing_depth_tac (Timing.start ()) cs) 0) i
    6.43       THEN flexflex_tac) st
    6.44      handle TRANS s =>
    6.45        ((if !trace then warning ("blast: " ^ s) else ());
    6.46 @@ -1299,7 +1299,7 @@
    6.47    let
    6.48      val state as State {fullTrace = ft, ...} = initialize thy;
    6.49      val res = timeap prove
    6.50 -      (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
    6.51 +      (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
    6.52      val _ = fullTrace := !ft;
    6.53    in res end;
    6.54  
     7.1 --- a/src/Pure/General/markup.ML	Sun Mar 20 21:20:07 2011 +0100
     7.2 +++ b/src/Pure/General/markup.ML	Sun Mar 20 21:28:11 2011 +0100
     7.3 @@ -100,7 +100,7 @@
     7.4    val elapsedN: string
     7.5    val cpuN: string
     7.6    val gcN: string
     7.7 -  val timingN: string val timing: timing -> T
     7.8 +  val timingN: string val timing: Timing.timing -> T
     7.9    val subgoalsN: string
    7.10    val proof_stateN: string val proof_state: int -> T
    7.11    val stateN: string val state: T
    7.12 @@ -312,7 +312,7 @@
    7.13  val cpuN = "cpu";
    7.14  val gcN = "gc";
    7.15  
    7.16 -fun timing ({elapsed, cpu, gc, ...}: timing) =
    7.17 +fun timing {elapsed, cpu, gc} =
    7.18    (timingN,
    7.19     [(elapsedN, Time.toString elapsed),
    7.20      (cpuN, Time.toString cpu),
     8.1 --- a/src/Pure/General/output.ML	Sun Mar 20 21:20:07 2011 +0100
     8.2 +++ b/src/Pure/General/output.ML	Sun Mar 20 21:28:11 2011 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      Pure/General/output.ML
     8.5      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     8.6  
     8.7 -Output channels and timing messages.
     8.8 +Isabelle output channels.
     8.9  *)
    8.10  
    8.11  signature BASIC_OUTPUT =
    8.12 @@ -10,11 +10,6 @@
    8.13    val tracing: string -> unit
    8.14    val warning: string -> unit
    8.15    val legacy_feature: string -> unit
    8.16 -  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
    8.17 -  val timeit: (unit -> 'a) -> 'a
    8.18 -  val timeap: ('a -> 'b) -> 'a -> 'b
    8.19 -  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    8.20 -  val timing: bool Unsynchronized.ref
    8.21  end;
    8.22  
    8.23  signature OUTPUT =
    8.24 @@ -111,31 +106,6 @@
    8.25  
    8.26  fun legacy_feature s = warning ("Legacy feature! " ^ s);
    8.27  
    8.28 -
    8.29 -
    8.30 -(** timing **)
    8.31 -
    8.32 -(*conditional timing with message*)
    8.33 -fun cond_timeit flag msg e =
    8.34 -  if flag then
    8.35 -    let
    8.36 -      val start = start_timing ();
    8.37 -      val result = Exn.capture e ();
    8.38 -      val end_msg = #message (end_timing start);
    8.39 -      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    8.40 -    in Exn.release result end
    8.41 -  else e ();
    8.42 -
    8.43 -(*unconditional timing*)
    8.44 -fun timeit e = cond_timeit true "" e;
    8.45 -
    8.46 -(*timed application function*)
    8.47 -fun timeap f x = timeit (fn () => f x);
    8.48 -fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
    8.49 -
    8.50 -(*global timing mode*)
    8.51 -val timing = Unsynchronized.ref false;
    8.52 -
    8.53  end;
    8.54  
    8.55  structure Basic_Output: BASIC_OUTPUT = Output;
     9.1 --- a/src/Pure/General/timing.ML	Sun Mar 20 21:20:07 2011 +0100
     9.2 +++ b/src/Pure/General/timing.ML	Sun Mar 20 21:28:11 2011 +0100
     9.3 @@ -4,19 +4,45 @@
     9.4  Basic support for time measurement.
     9.5  *)
     9.6  
     9.7 -val seconds = Time.fromReal;
     9.8 +signature BASIC_TIMING =
     9.9 +sig
    9.10 +  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
    9.11 +  val timeit: (unit -> 'a) -> 'a
    9.12 +  val timeap: ('a -> 'b) -> 'a -> 'b
    9.13 +  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    9.14 +end
    9.15  
    9.16 -fun start_timing () =
    9.17 +signature TIMING =
    9.18 +sig
    9.19 +  include BASIC_TIMING
    9.20 +  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
    9.21 +  type start
    9.22 +  val start: unit -> start
    9.23 +  val result: start -> timing
    9.24 +  val message: timing -> string
    9.25 +end
    9.26 +
    9.27 +structure Timing: TIMING =
    9.28 +struct
    9.29 +
    9.30 +(* timer control *)
    9.31 +
    9.32 +type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
    9.33 +
    9.34 +abstype start = Start of
    9.35 +  Timer.real_timer * Time.time * Timer.cpu_timer *
    9.36 +    {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
    9.37 +with
    9.38 +
    9.39 +fun start () =
    9.40    let
    9.41      val real_timer = Timer.startRealTimer ();
    9.42      val real_time = Timer.checkRealTimer real_timer;
    9.43      val cpu_timer = Timer.startCPUTimer ();
    9.44      val cpu_times = Timer.checkCPUTimes cpu_timer;
    9.45 -  in (real_timer, real_time, cpu_timer, cpu_times) end;
    9.46 +  in Start (real_timer, real_time, cpu_timer, cpu_times) end;
    9.47  
    9.48 -type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
    9.49 -
    9.50 -fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
    9.51 +fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
    9.52    let
    9.53      val real_time2 = Timer.checkRealTimer real_timer;
    9.54      val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    9.55 @@ -27,10 +53,34 @@
    9.56      val elapsed = real_time2 - real_time;
    9.57      val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    9.58      val cpu = usr2 - usr + sys2 - sys + gc;
    9.59 +  in {elapsed = elapsed, cpu = cpu, gc = gc} end;
    9.60  
    9.61 -    val message =
    9.62 -     (toString elapsed ^ "s elapsed time, " ^
    9.63 -      toString cpu ^ "s cpu time, " ^
    9.64 -      toString gc ^ "s GC time") handle Time.Time => "";
    9.65 -  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
    9.66 +end;
    9.67 +
    9.68 +
    9.69 +(* timing messages *)
    9.70 +
    9.71 +fun message {elapsed, cpu, gc} =
    9.72 +  Time.toString elapsed ^ "s elapsed time, " ^
    9.73 +  Time.toString cpu ^ "s cpu time, " ^
    9.74 +  Time.toString gc ^ "s GC time" handle Time.Time => "";
    9.75  
    9.76 +fun cond_timeit enabled msg e =
    9.77 +  if enabled then
    9.78 +    let
    9.79 +      val timing_start = start ();
    9.80 +      val res = Exn.capture e ();
    9.81 +      val end_msg = message (result timing_start);
    9.82 +      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    9.83 +    in Exn.release res end
    9.84 +  else e ();
    9.85 +
    9.86 +fun timeit e = cond_timeit true "" e;
    9.87 +fun timeap f x = timeit (fn () => f x);
    9.88 +fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
    9.89 +
    9.90 +end;
    9.91 +
    9.92 +structure Basic_Timing: BASIC_TIMING = Timing;
    9.93 +open Basic_Timing;
    9.94 +
    10.1 --- a/src/Pure/IsaMakefile	Sun Mar 20 21:20:07 2011 +0100
    10.2 +++ b/src/Pure/IsaMakefile	Sun Mar 20 21:28:11 2011 +0100
    10.3 @@ -21,7 +21,6 @@
    10.4  
    10.5  BOOTSTRAP_FILES = 					\
    10.6    General/exn.ML					\
    10.7 -  General/timing.ML					\
    10.8    ML-Systems/compiler_polyml-5.2.ML			\
    10.9    ML-Systems/compiler_polyml-5.3.ML			\
   10.10    ML-Systems/ml_name_space.ML				\
   10.11 @@ -101,6 +100,7 @@
   10.12    General/symbol.ML					\
   10.13    General/symbol_pos.ML					\
   10.14    General/table.ML					\
   10.15 +  General/timing.ML					\
   10.16    General/url.ML					\
   10.17    General/xml.ML					\
   10.18    General/xml_data.ML					\
    11.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 20 21:20:07 2011 +0100
    11.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 20 21:28:11 2011 +0100
    11.3 @@ -271,7 +271,7 @@
    11.4  fun load_thy name init pos text =
    11.5    let
    11.6      val (lexs, commands) = get_syntax ();
    11.7 -    val time = ! Output.timing;
    11.8 +    val time = ! Toplevel.timing;
    11.9  
   11.10      val _ = Present.init_theory name;
   11.11  
    12.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 20 21:20:07 2011 +0100
    12.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 20 21:28:11 2011 +0100
    12.3 @@ -218,7 +218,7 @@
    12.4  val quiet = Unsynchronized.ref false;
    12.5  val debug = Runtime.debug;
    12.6  val interact = Unsynchronized.ref false;
    12.7 -val timing = Output.timing;
    12.8 +val timing = Unsynchronized.ref false;
    12.9  val profiling = Unsynchronized.ref 0;
   12.10  val skip_proofs = Unsynchronized.ref false;
   12.11  
    13.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Sun Mar 20 21:20:07 2011 +0100
    13.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sun Mar 20 21:28:11 2011 +0100
    13.3 @@ -14,10 +14,12 @@
    13.4  else use "ML-Systems/single_assignment_polyml.ML";
    13.5  
    13.6  use "ML-Systems/multithreading.ML";
    13.7 -use "General/timing.ML";
    13.8  use "ML-Systems/ml_pretty.ML";
    13.9  use "ML-Systems/use_context.ML";
   13.10  
   13.11 +val seconds = Time.fromReal;
   13.12 +
   13.13 +
   13.14  
   13.15  (** ML system and platform related **)
   13.16  
    14.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Mar 20 21:20:07 2011 +0100
    14.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Mar 20 21:28:11 2011 +0100
    14.3 @@ -13,7 +13,6 @@
    14.4  use "ML-Systems/universal.ML";
    14.5  use "ML-Systems/thread_dummy.ML";
    14.6  use "ML-Systems/multithreading.ML";
    14.7 -use "General/timing.ML";
    14.8  use "ML-Systems/ml_name_space.ML";
    14.9  use "ML-Systems/ml_pretty.ML";
   14.10  structure PolyML = struct end;
   14.11 @@ -21,8 +20,9 @@
   14.12  use "ML-Systems/use_context.ML";
   14.13  
   14.14  
   14.15 +val seconds = Time.fromReal;
   14.16 +
   14.17  (*low-level pointer equality*)
   14.18 -
   14.19  CM.autoload "$smlnj/init/init.cmi";
   14.20  val pointer_eq = InlineT.ptreql;
   14.21  
    15.1 --- a/src/Pure/PIDE/document.ML	Sun Mar 20 21:20:07 2011 +0100
    15.2 +++ b/src/Pure/PIDE/document.ML	Sun Mar 20 21:28:11 2011 +0100
    15.3 @@ -241,9 +241,9 @@
    15.4          val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    15.5          val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
    15.6  
    15.7 -        val start = start_timing ();
    15.8 +        val start = Timing.start ();
    15.9          val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   15.10 -        val _ = timing tr (end_timing start);
   15.11 +        val _ = timing tr (Timing.result start);
   15.12          val _ = List.app (Toplevel.error_msg tr) errs;
   15.13          val res =
   15.14            (case result of
    16.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sun Mar 20 21:20:07 2011 +0100
    16.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sun Mar 20 21:28:11 2011 +0100
    16.3 @@ -156,7 +156,7 @@
    16.4    bool_pref Pattern.trace_unify_fail
    16.5      "trace-unification"
    16.6      "Output error diagnostics during unification",
    16.7 -  bool_pref Output.timing
    16.8 +  bool_pref Toplevel.timing
    16.9      "global-timing"
   16.10      "Whether to enable timing in Isabelle.",
   16.11    bool_pref Toplevel.debug
    17.1 --- a/src/Pure/ROOT.ML	Sun Mar 20 21:20:07 2011 +0100
    17.2 +++ b/src/Pure/ROOT.ML	Sun Mar 20 21:28:11 2011 +0100
    17.3 @@ -21,6 +21,7 @@
    17.4  use "General/alist.ML";
    17.5  use "General/table.ML";
    17.6  use "General/output.ML";
    17.7 +use "General/timing.ML";
    17.8  use "General/properties.ML";
    17.9  use "General/markup.ML";
   17.10  use "General/scan.ML";
    18.1 --- a/src/Pure/System/session.ML	Sun Mar 20 21:20:07 2011 +0100
    18.2 +++ b/src/Pure/System/session.ML	Sun Mar 20 21:28:11 2011 +0100
    18.3 @@ -101,13 +101,12 @@
    18.4          (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
    18.5        if timing then
    18.6          let
    18.7 -          val start = start_timing ();
    18.8 +          val start = Timing.start ();
    18.9            val _ = use root;
   18.10 -          val stop = end_timing start;
   18.11            val _ =
   18.12              Output.raw_stderr ("Timing " ^ item ^ " (" ^
   18.13                string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
   18.14 -              #message stop ^ ")\n");
   18.15 +              Timing.message (Timing.result start) ^ ")\n");
   18.16          in () end
   18.17        else use root;
   18.18        finish ()))
    19.1 --- a/src/Pure/Tools/find_consts.ML	Sun Mar 20 21:20:07 2011 +0100
    19.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Mar 20 21:28:11 2011 +0100
    19.3 @@ -69,7 +69,7 @@
    19.4  
    19.5  fun find_consts ctxt raw_criteria =
    19.6    let
    19.7 -    val start = start_timing ();
    19.8 +    val start = Timing.start ();
    19.9  
   19.10      val thy = ProofContext.theory_of ctxt;
   19.11      val low_ranking = 10000;
   19.12 @@ -114,7 +114,7 @@
   19.13        |> sort (rev_order o int_ord o pairself snd)
   19.14        |> map (apsnd fst o fst);
   19.15  
   19.16 -    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   19.17 +    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   19.18    in
   19.19      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
   19.20      Pretty.str "" ::
    20.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 20 21:20:07 2011 +0100
    20.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 20 21:28:11 2011 +0100
    20.3 @@ -464,7 +464,7 @@
    20.4  
    20.5  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    20.6    let
    20.7 -    val start = start_timing ();
    20.8 +    val start = Timing.start ();
    20.9  
   20.10      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   20.11      val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
   20.12 @@ -480,7 +480,7 @@
   20.13               then " (" ^ string_of_int returned ^ " displayed)"
   20.14               else ""));
   20.15  
   20.16 -    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   20.17 +    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
   20.18    in
   20.19      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
   20.20      Pretty.str "" ::
    21.1 --- a/src/Tools/quickcheck.ML	Sun Mar 20 21:20:07 2011 +0100
    21.2 +++ b/src/Tools/quickcheck.ML	Sun Mar 20 21:28:11 2011 +0100
    21.3 @@ -167,11 +167,11 @@
    21.4      val frees = Term.add_frees t [];
    21.5    in (frees, list_abs_free (frees, t)) end
    21.6  
    21.7 -fun cpu_time description f =
    21.8 +fun cpu_time description f =  (* FIXME !? *)
    21.9    let
   21.10 -    val start = start_timing ()
   21.11 +    val start = Timing.start ()
   21.12      val result = Exn.capture f ()
   21.13 -    val time = Time.toMilliseconds (#cpu (end_timing start))
   21.14 +    val time = Time.toMilliseconds (#cpu (Timing.result start))
   21.15    in (Exn.release result, (description, time)) end
   21.16  
   21.17  fun limit ctxt (limit_time, is_interactive) f exc () =