# HG changeset patch
# User wenzelm
# Date 1495726355 -7200
# Node ID 5b42937d3b2d852aa5a6cbf8b0229198df89a1ac
# Parent  9e65c03e94da239bf750293f8e4008b94645f921
more operations;

diff -r 9e65c03e94da -r 5b42937d3b2d src/Pure/General/logger.scala
--- 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
diff -r 9e65c03e94da -r 5b42937d3b2d src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu May 25 17:28:11 2017 +0200
+++ b/src/Pure/System/progress.scala	Thu May 25 17:32:35 2017 +0200
@@ -19,6 +19,9 @@
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
 
+  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
+    Timing.timeit(message, enabled, echo(_))(e)
+
   def stopped: Boolean = false
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"