# HG changeset patch
# User wenzelm
# Date 1670424227 -3600
# Node ID ec8bf1268f45700b3127048fbf07085f901ba90c
# Parent  b9a7a658f7df1cad327d1eb5ae172ca67d1dfcdb
tuned signature: more operations;

diff -r b9a7a658f7df -r ec8bf1268f45 src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Wed Dec 07 12:41:31 2022 +0100
+++ b/src/Pure/General/logger.scala	Wed Dec 07 15:43:47 2022 +0100
@@ -18,8 +18,13 @@
 trait Logger {
   def apply(msg: => String): Unit
 
-  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
-    Timing.timeit(message, enabled, apply(_))(e)
+  def timeit_result[A](
+    message: Exn.Result[A] => String = null,
+    enabled: Boolean = true
+  )(e: => A): A = Timing.timeit_result(message, enabled, apply(_))(e)
+
+  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A) =
+    timeit_result(_ => message, enabled)
 }
 
 object No_Logger extends Logger {
diff -r b9a7a658f7df -r ec8bf1268f45 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Wed Dec 07 12:41:31 2022 +0100
+++ b/src/Pure/General/timing.scala	Wed Dec 07 15:43:47 2022 +0100
@@ -13,8 +13,8 @@
 object Timing {
   val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
 
-  def timeit[A](
-    message: String = "",
+  def timeit_result[A](
+    message: Exn.Result[A] => String = null,
     enabled: Boolean = true,
     output: String => Unit = Output.warning(_)
   )(e: => A): A = {
@@ -25,9 +25,8 @@
 
       val timing = stop - start
       if (timing.is_relevant) {
-        output(
-          (if (message == null || message == "") "" else message + ": ") +
-            timing.message + " elapsed time")
+        val msg = if (message == null) null else message(result)
+        output((if (msg == null || msg == "") "" else msg + ": ") + timing.message + " elapsed time")
       }
 
       Exn.release(result)
@@ -35,6 +34,12 @@
     else e
   }
 
+  def timeit[A](
+    message: String = "",
+    enabled: Boolean = true,
+    output: String => Unit = Output.warning(_)
+  )(e: => A): A = timeit_result[A](_ => message, enabled, output)(e)
+
   def factor_format(f: Double): String =
     String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
 }
diff -r b9a7a658f7df -r ec8bf1268f45 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Dec 07 12:41:31 2022 +0100
+++ b/src/Pure/System/progress.scala	Wed Dec 07 15:43:47 2022 +0100
@@ -31,8 +31,15 @@
   def echo_warning(msg: String): Unit = echo(Output.warning_text(msg))
   def echo_error_message(msg: String): Unit = echo(Output.error_message_text(msg))
 
-  def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
-    Timing.timeit(message, enabled, echo)(e)
+  def timeit_result[A](
+    message: Exn.Result[A] => String = null,
+    enabled: Boolean = true
+  )(e: => A): A = Timing.timeit_result(message, enabled, echo)(e)
+
+  def timeit[A](
+    message: String = "",
+    enabled: Boolean = true
+  )(e: => A): A = timeit_result[A](_ => message, enabled)(e)
 
   @volatile protected var is_stopped = false
   def stop(): Unit = { is_stopped = true }