# HG changeset patch # User wenzelm # Date 1235920957 -3600 # Node ID 82144a95f9ec8bcdeda4dc7929d19a89318b382d # Parent b92b3375e91934a92bae881d4b574e36d0aeec2a avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example; diff -r b92b3375e919 -r 82144a95f9ec src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Sun Mar 01 16:21:33 2009 +0100 +++ b/src/Pure/Tools/find_consts.ML Sun Mar 01 16:22:37 2009 +0100 @@ -119,9 +119,7 @@ |> sort (rev_order o int_ord o pairself snd) |> map ((apsnd fst) o fst); - val end_msg = " in " ^ - (List.nth (String.tokens Char.isSpace (end_timing start), 3)) - ^ " secs" + val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; in Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: Pretty.str "" diff -r b92b3375e919 -r 82144a95f9ec src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sun Mar 01 16:21:33 2009 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sun Mar 01 16:22:37 2009 +0100 @@ -372,9 +372,7 @@ val lim = the_default (! limit) opt_limit; val thms = Library.drop (len - lim, matches); - val end_msg = " in " ^ - (List.nth (String.tokens Char.isSpace (end_timing start), 3)) - ^ " secs" + val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; in Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::