src/Pure/ML-Systems/smlnj-0.93.ML
changeset 3631 88a279998f90
parent 3595 fb25f00d1c70
child 4340 f5d7fbb73103
equal deleted inserted replaced
3630:aee7effe0816 3631:88a279998f90
    28 
    28 
    29 
    29 
    30 (* timing *)
    30 (* timing *)
    31 
    31 
    32 local
    32 local
    33 
    33   (*print microseconds, suppressing trailing zeroes*)
    34 (*print microseconds, suppressing trailing zeroes*)
    34   fun umakestring 0 = ""
    35 fun umakestring 0 = ""
    35     | umakestring n =
    36   | umakestring n =
    36         chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
    37       chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
       
    38 
       
    39 in
    37 in
    40 
    38   (*a conditional timing function: applies f to () and, if the flag is true,
    41 (*a conditional timing function: applies f to () and, if the flag is true,
    39     prints its runtime*)
    42   prints its runtime*)
    40   fun cond_timeit flag f =
    43 
    41     if flag then
    44 fun cond_timeit flag f =
    42       let fun string_of_time (System.Timer.TIME {sec, usec}) =
    45   if flag then
    43               makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
    46     let fun string_of_time (System.Timer.TIME {sec, usec}) =
    44           open System.Timer;
    47             makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
    45           val start = start_timer()
    48         open System.Timer;
    46           val result = f();
    49         val start = start_timer()
    47           val nongc = check_timer(start)
    50         val result = f();
    48           and gc = check_timer_gc(start);
    51         val nongc = check_timer(start)
    49           val both = add_time(nongc, gc)
    52         and gc = check_timer_gc(start);
    50       in  print("Non GC " ^ string_of_time nongc ^
    53         val both = add_time(nongc, gc)
    51                  "   GC " ^ string_of_time gc ^
    54     in  print("Non GC " ^ string_of_time nongc ^
    52                  "  both "^ string_of_time both ^ " secs\n");
    55                "   GC " ^ string_of_time gc ^
    53           result
    56                "  both "^ string_of_time both ^ " secs\n");
    54       end
    57         result
    55     else f();
    58     end
       
    59   else f();
       
    60 
       
    61 end;
    56 end;
    62 
    57 
    63 
    58 
    64 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    59 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    65 
    60 
    79 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    74 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    80 
    75 
    81 
    76 
    82 (* ML command execution *)
    77 (* ML command execution *)
    83 
    78 
    84 fun use_string commands =
    79 fun use_strings commands =
    85   System.Compile.use_stream (open_string (implode commands));
    80   System.Compile.use_stream (open_string (implode commands));
    86 
    81 
    87 
    82 
    88 
    83 
    89 (** OS related **)
    84 (** OS related **)