discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
authorwenzelm
Mon Feb 27 19:54:50 2012 +0100 (2012-02-27)
changeset 46716c45a4427db39
parent 46715 6236ca7b32a7
child 46717 b09afce1e54f
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 19:53:34 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 19:54:50 2012 +0100
     1.3 @@ -84,7 +84,6 @@
     1.4  
     1.5  fun print_unused_assms ctxt opt_thy_name =
     1.6    let
     1.7 -    val start = Timing.start ()
     1.8      val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
     1.9      val results = find_unused_assms ctxt thy_name
    1.10      val total = length results
    1.11 @@ -97,7 +96,6 @@
    1.12      val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
    1.13        ^ " in the theory " ^ quote thy_name
    1.14        ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
    1.15 -      ^ " in " ^ Timing.message (Timing.result start);
    1.16    in
    1.17      ([Pretty.str (msg ^ ":"), Pretty.str ""] @
    1.18          map pretty_thm with_superfluous_assumptions
     2.1 --- a/src/Pure/Tools/find_consts.ML	Mon Feb 27 19:53:34 2012 +0100
     2.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Feb 27 19:54:50 2012 +0100
     2.3 @@ -69,8 +69,6 @@
     2.4  
     2.5  fun find_consts ctxt raw_criteria =
     2.6    let
     2.7 -    val start = Timing.start ();
     2.8 -
     2.9      val thy = Proof_Context.theory_of ctxt;
    2.10      val low_ranking = 10000;
    2.11  
    2.12 @@ -113,15 +111,13 @@
    2.13        |> map_filter I
    2.14        |> sort (rev_order o int_ord o pairself snd)
    2.15        |> map (apsnd fst o fst);
    2.16 -
    2.17 -    val end_msg = " in " ^ Timing.message (Timing.result start);
    2.18    in
    2.19      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    2.20      Pretty.str "" ::
    2.21      Pretty.str
    2.22       (if null matches
    2.23 -      then "nothing found" ^ end_msg
    2.24 -      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
    2.25 +      then "nothing found"
    2.26 +      else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
    2.27      Pretty.str "" ::
    2.28      map (pretty_const ctxt) matches
    2.29    end |> Pretty.chunks |> Pretty.writeln;
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:53:34 2012 +0100
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:54:50 2012 +0100
     3.3 @@ -586,8 +586,6 @@
     3.4  
     3.5  fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
     3.6    let
     3.7 -    val start = Timing.start ();
     3.8 -
     3.9      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    3.10      val (foundo, theorems) = find
    3.11        {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
    3.12 @@ -601,14 +599,12 @@
    3.13              (if returned < found
    3.14               then " (" ^ string_of_int returned ^ " displayed)"
    3.15               else ""));
    3.16 -
    3.17 -    val end_msg = " in " ^ Timing.message (Timing.result start);
    3.18    in
    3.19      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    3.20      Pretty.str "" ::
    3.21 -    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
    3.22 +    (if null theorems then [Pretty.str "nothing found"]
    3.23       else
    3.24 -      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
    3.25 +      [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
    3.26          map (pretty_theorem ctxt) theorems)
    3.27    end |> Pretty.chunks |> Pretty.writeln;
    3.28