tuned;
authorwenzelm
Thu Jul 19 23:18:46 2007 +0200 (2007-07-19)
changeset 23862b1861768d8f4
parent 23861 72bb3494746f
child 23863 8f3099589cfa
tuned;
src/Pure/General/output.ML
     1.1 --- a/src/Pure/General/output.ML	Thu Jul 19 23:18:45 2007 +0200
     1.2 +++ b/src/Pure/General/output.ML	Thu Jul 19 23:18:46 2007 +0200
     1.3 @@ -141,16 +141,16 @@
     1.4  (*global timing mode*)
     1.5  val timing = ref false;
     1.6  
     1.7 -(*a conditional timing function: applies f to () and, if the flag is true,
     1.8 -  prints its runtime on warning channel*)
     1.9 +(*conditional timing*)
    1.10  fun cond_timeit flag f =
    1.11    if flag then
    1.12 -    let val start = start_timing ()
    1.13 -        val result = f ()
    1.14 +    let
    1.15 +      val start = start_timing ();
    1.16 +      val result = f ();
    1.17      in warning (end_timing start); result end
    1.18    else f ();
    1.19  
    1.20 -(*unconditional timing function*)
    1.21 +(*unconditional timing*)
    1.22  fun timeit x = cond_timeit true x;
    1.23  
    1.24  (*timed application function*)