cleaned up;
authorwenzelm
Tue Aug 05 17:03:11 1997 +0200 (1997-08-05)
changeset 3595fb25f00d1c70
parent 3594 193cc37e6f60
child 3596 c44c83006891
cleaned up;
added getenv;
src/Pure/ML-Systems/smlnj-0.93.ML
     1.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML	Tue Aug 05 17:02:50 1997 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Tue Aug 05 17:03:11 1997 +0200
     1.3 @@ -30,29 +30,34 @@
     1.4  (* timing *)
     1.5  
     1.6  local
     1.7 -  (*print microseconds, suppressing trailing zeroes*)
     1.8 -  fun umakestring 0 = ""
     1.9 -    | umakestring n =
    1.10 -        chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
    1.11 +
    1.12 +(*print microseconds, suppressing trailing zeroes*)
    1.13 +fun umakestring 0 = ""
    1.14 +  | umakestring n =
    1.15 +      chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
    1.16 +
    1.17  in
    1.18 -  (*a conditional timing function: applies f to () and, if the flag is true,
    1.19 -    prints its runtime*)
    1.20 -  fun cond_timeit flag f =
    1.21 -    if flag then
    1.22 -      let fun string_of_time (System.Timer.TIME {sec, usec}) =
    1.23 -              makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
    1.24 -          open System.Timer;
    1.25 -          val start = start_timer()
    1.26 -          val result = f();
    1.27 -          val nongc = check_timer(start)
    1.28 -          and gc = check_timer_gc(start);
    1.29 -          val both = add_time(nongc, gc)
    1.30 -      in  print("Non GC " ^ string_of_time nongc ^
    1.31 -                 "   GC " ^ string_of_time gc ^
    1.32 -                 "  both "^ string_of_time both ^ " secs\n");
    1.33 -          result
    1.34 -      end
    1.35 -    else f();
    1.36 +
    1.37 +(*a conditional timing function: applies f to () and, if the flag is true,
    1.38 +  prints its runtime*)
    1.39 +
    1.40 +fun cond_timeit flag f =
    1.41 +  if flag then
    1.42 +    let fun string_of_time (System.Timer.TIME {sec, usec}) =
    1.43 +            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
    1.44 +        open System.Timer;
    1.45 +        val start = start_timer()
    1.46 +        val result = f();
    1.47 +        val nongc = check_timer(start)
    1.48 +        and gc = check_timer_gc(start);
    1.49 +        val both = add_time(nongc, gc)
    1.50 +    in  print("Non GC " ^ string_of_time nongc ^
    1.51 +               "   GC " ^ string_of_time gc ^
    1.52 +               "  both "^ string_of_time both ^ " secs\n");
    1.53 +        result
    1.54 +    end
    1.55 +  else f();
    1.56 +
    1.57  end;
    1.58  
    1.59