src/Pure/General/output.ML
changeset 23862 b1861768d8f4
parent 23727 39f8d1480d55
child 23922 707639e9497d
     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*)