Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more detailed start_timing/end_timing;
authorwenzelm
Wed, 17 Jun 2009 17:07:26 +0200
changeset 31687 0d2f700fe5e7
parent 31686 e54ae15335a1
child 31688 f27cc190083b
more detailed start_timing/end_timing;
src/Pure/Tools/find_consts.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/find_consts.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Jun 17 17:07:26 2009 +0200
@@ -128,7 +128,7 @@
       |> sort (rev_order o int_ord o pairself snd)
       |> map (apsnd fst o fst);
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
       :: Pretty.str ""
--- a/src/Pure/Tools/find_theorems.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Jun 17 17:07:26 2009 +0200
@@ -427,7 +427,7 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
         :: Pretty.str "" ::
isabelle