--- a/src/Pure/General/logger.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Pure/General/logger.scala Wed Dec 07 21:03:17 2022 +0100
@@ -18,8 +18,10 @@
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[A](body: => A,
+ message: Exn.Result[A] => String = null,
+ enabled: Boolean = true
+ ): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_))
}
object No_Logger extends Logger {
--- a/src/Pure/General/timing.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Pure/General/timing.scala Wed Dec 07 21:03:17 2022 +0100
@@ -13,26 +13,25 @@
object Timing {
val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
- def timeit[A](
- message: String = "",
+ 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
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)
}
- else e
+ else body
}
def factor_format(f: Double): String =
--- a/src/Pure/PIDE/resources.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Wed Dec 07 21:03:17 2022 +0100
@@ -267,9 +267,9 @@
/* blobs */
- def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
+ def undefined_blobs(version: Document.Version): List[Document.Node.Name] =
(for {
- (node_name, node) <- nodes.iterator
+ (node_name, node) <- version.nodes.iterator
if !session_base.loaded_theory(node_name)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
--- a/src/Pure/PIDE/session.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Pure/PIDE/session.scala Wed Dec 07 21:03:17 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
@@ -690,6 +691,10 @@
get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
resources.session_base.overall_syntax
+ def stable_tip_version[A](models: Map[A, Document.Model]): Option[Document.Version] =
+ if (models.valuesIterator.forall(_.is_stable)) get_state().stable_tip_version
+ else None
+
@tailrec final def await_stable_snapshot(): Document.Snapshot = {
val snapshot = this.snapshot()
if (snapshot.is_outdated) {
--- a/src/Pure/System/progress.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Pure/System/progress.scala Wed Dec 07 21:03:17 2022 +0100
@@ -31,8 +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[A](message: String = "", enabled: Boolean = true)(e: => A): A =
- Timing.timeit(message, enabled, echo)(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 }
--- a/src/Tools/VSCode/src/language_server.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Wed Dec 07 21:03:17 2022 +0100
@@ -283,8 +283,9 @@
val resources =
new VSCode_Resources(options, base_info, log) {
override def commit(change: Session.Change): Unit =
- if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
+ if (change.deps_changed || undefined_blobs(change.version).nonEmpty) {
delay_load.invoke()
+ }
}
val session_options = options.bool("editor_output_state") = true
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Dec 07 21:03:17 2022 +0100
@@ -208,19 +208,10 @@
file_watcher: File_Watcher
): (Boolean, Boolean) = {
state.change_result { st =>
- val thy_files = resources.resolve_dependencies(st.models, Nil)
+ val stable_tip_version = session.stable_tip_version(st.models)
- val stable_tip_version =
- if (st.models.valuesIterator.forall(_.is_stable)) {
- session.get_state().stable_tip_version
- }
- else None
-
- val aux_files =
- stable_tip_version match {
- case Some(version) => undefined_blobs(version.nodes)
- case None => Nil
- }
+ val thy_files = resources.resolve_dependencies(st.models, Nil)
+ val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
val loaded_models =
(for {
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 07 21:03:17 2022 +0100
@@ -133,7 +133,7 @@
if (change.syntax_changed.nonEmpty)
GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
if (change.deps_changed ||
- PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
+ PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version).nonEmpty)
PIDE.plugin.deps_changed()
}
}
--- a/src/Tools/jEdit/src/main_plugin.scala Wed Dec 07 10:11:58 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Wed Dec 07 21:03:17 2022 +0100
@@ -118,13 +118,8 @@
val aux_files =
if (options.bool("jedit_auto_resolve")) {
- val stable_tip_version =
- if (models.valuesIterator.forall(_.is_stable)) {
- session.get_state().stable_tip_version
- }
- else None
- stable_tip_version match {
- case Some(version) => resources.undefined_blobs(version.nodes)
+ session.stable_tip_version(models) match {
+ case Some(version) => resources.undefined_blobs(version)
case None => delay_load.invoke(); Nil
}
}