src/Pure/library.ML

 
   (*timing*)
   val cond_timeit: bool -> (unit -> 'a) -> 'a
   val timeit: (unit -> 'a) -> 'a
   val timeap: ('a -> 'b) -> 'a -> 'b
+  val timing: bool ref
 
   (*misc*)
   val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
   val keyfilter: ('a * ''b) list -> ''b -> 'a list
   val partition: ('a -> bool) -> 'a list -> 'a list * 'a list

 
 
 (** timing **)
 
 (*a conditional timing function: applies f to () and, if the flag is true,
-  prints its runtime*)
+  prints its runtime on warning channel*)
 fun cond_timeit flag f =
   if flag then
     let val start = startTiming()
         val result = f ()
-    in
-        writeln (endTiming start);  result
-    end
+    in warning (endTiming start);  result end
   else f ();
 
 (*unconditional timing function*)
 fun timeit x = cond_timeit true x;
 
 (*timed application function*)
 fun timeap f x = timeit (fn () => f x);
+
+(*global timing mode*)
+val timing = ref false;
 
 
 
 (** misc **)