avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
authorwenzelm
Sun Mar 01 16:22:37 2009 +0100 (2009-03-01)
changeset 3018882144a95f9ec
parent 30187 b92b3375e919
child 30189 3633f560f4c3
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:21:33 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:22:37 2009 +0100
     1.3 @@ -119,9 +119,7 @@
     1.4        |> sort (rev_order o int_ord o pairself snd)
     1.5        |> map ((apsnd fst) o fst);
     1.6  
     1.7 -    val end_msg = " in " ^
     1.8 -                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
     1.9 -                  ^ " secs"
    1.10 +    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
    1.11    in
    1.12      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    1.13        :: Pretty.str ""
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:21:33 2009 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:22:37 2009 +0100
     2.3 @@ -372,9 +372,7 @@
     2.4      val lim = the_default (! limit) opt_limit;
     2.5      val thms = Library.drop (len - lim, matches);
     2.6  
     2.7 -    val end_msg = " in " ^
     2.8 -                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
     2.9 -                  ^ " secs"
    2.10 +    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
    2.11    in
    2.12      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
    2.13          :: Pretty.str "" ::