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