src/Pure/General/logger.scala
changeset 65921 5b42937d3b2d
parent 64606 a871fa7c24fc
child 73340 0ffcad1f6130
--- a/src/Pure/General/logger.scala	Thu May 25 17:28:11 2017 +0200
+++ b/src/Pure/General/logger.scala	Thu May 25 17:32:35 2017 +0200
@@ -16,6 +16,9 @@
 trait Logger
 {
   def apply(msg: => String): Unit
+
+  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
+    Timing.timeit(message, enabled, apply(_))(e)
 }
 
 object No_Logger extends Logger