src/Pure/General/timing.scala

--- a/src/Pure/General/timing.scala	Wed Dec 07 15:43:47 2022 +0100
+++ b/src/Pure/General/timing.scala	Wed Dec 07 21:02:43 2022 +0100
@@ -13,14 +13,14 @@
 object Timing {
   val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
 
-  def timeit_result[A](
+  def timeit[A](body: => A,
     message: Exn.Result[A] => String = null,
     enabled: Boolean = true,
     output: String => Unit = Output.warning(_)
-  )(e: => A): A = {
+  ): A = {
     if (enabled) {
       val start = Time.now()
-      val result = Exn.capture(e)
+      val result = Exn.capture(body)
       val stop = Time.now()
 
       val timing = stop - start
@@ -31,15 +31,9 @@
 
       Exn.release(result)
     }
-    else e
+    else body
   }
 
-  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))
 }