# HG changeset patch
# User wenzelm
# Date 1670443363 -3600
# Node ID badb5264f7b9b0969dfd282e488ddf805de18fd6
# Parent  ec8bf1268f45700b3127048fbf07085f901ba90c
clarified signature: just one level of arguments to avoid type-inference problems;

diff -r ec8bf1268f45 -r badb5264f7b9 src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Wed Dec 07 15:43:47 2022 +0100
+++ b/src/Pure/General/logger.scala	Wed Dec 07 21:02:43 2022 +0100
@@ -18,13 +18,10 @@
 trait Logger {
   def apply(msg: => String): Unit
 
-  def timeit_result[A](
+  def timeit[A](body: => 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)
+  ): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_))
 }
 
 object No_Logger extends Logger {
diff -r ec8bf1268f45 -r badb5264f7b9 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))
 }
diff -r ec8bf1268f45 -r badb5264f7b9 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Dec 07 15:43:47 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Dec 07 21:02:43 2022 +0100
@@ -241,9 +241,10 @@
     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
       val prev = previous.get_finished
       val change =
-        Timing.timeit("parse_change", timing) {
-          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
-        }
+        Timing.timeit(
+          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate),
+          message = _ => "parse_change",
+          enabled = timing)
       version_result.fulfill(change.version)
       manager.send(change)
       true
diff -r ec8bf1268f45 -r badb5264f7b9 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Dec 07 15:43:47 2022 +0100
+++ b/src/Pure/System/progress.scala	Wed Dec 07 21:02:43 2022 +0100
@@ -31,15 +31,8 @@
   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_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)
+  def timeit[A](body: => A, message: Exn.Result[A] => String = null, enabled: Boolean = true): A =
+    Timing.timeit(body, message = message, enabled = enabled, output = echo)
 
   @volatile protected var is_stopped = false
   def stop(): Unit = { is_stopped = true }