src/Pure/library.ML
changeset 4326 7211ea5f29e2
parent 4284 eb65491ae776
child 4343 9849fb57c395
     1.1 --- a/src/Pure/library.ML	Fri Nov 28 10:54:13 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Nov 28 10:59:14 1997 +0100
     1.3 @@ -802,6 +802,17 @@
     1.4  
     1.5  (** timing **)
     1.6  
     1.7 +(*a conditional timing function: applies f to () and, if the flag is true,
     1.8 +  prints its runtime*)
     1.9 +fun cond_timeit flag f =
    1.10 +  if flag then
    1.11 +    let val start = startTiming()
    1.12 +        val result = f ()
    1.13 +    in
    1.14 +	writeln (endTiming start);  result
    1.15 +    end
    1.16 +  else f ();
    1.17 +
    1.18  (*unconditional timing function*)
    1.19  fun timeit x = cond_timeit true x;
    1.20