more operations;

--- 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

--- 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"