clarified signature: just one level of arguments to avoid type-inference problems;
--- 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 {
--- 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))
}
--- 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
--- 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 }