# HG changeset patch # User wenzelm # Date 1670443397 -3600 # Node ID 186dcfe746e33ba6ff957dd4a273d556dd0f15b1 # Parent 1c083e32aed6380b24dd5dbe8a48ce9fcdaac73d# Parent badb5264f7b9b0969dfd282e488ddf805de18fd6 merged diff -r 1c083e32aed6 -r 186dcfe746e3 src/Pure/General/logger.scala --- 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 { diff -r 1c083e32aed6 -r 186dcfe746e3 src/Pure/General/timing.scala --- 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 = diff -r 1c083e32aed6 -r 186dcfe746e3 src/Pure/PIDE/resources.scala --- 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 diff -r 1c083e32aed6 -r 186dcfe746e3 src/Pure/PIDE/session.scala --- 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) { diff -r 1c083e32aed6 -r 186dcfe746e3 src/Pure/System/progress.scala --- 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 } diff -r 1c083e32aed6 -r 186dcfe746e3 src/Tools/VSCode/src/language_server.scala --- 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 diff -r 1c083e32aed6 -r 186dcfe746e3 src/Tools/VSCode/src/vscode_resources.scala --- 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 { diff -r 1c083e32aed6 -r 186dcfe746e3 src/Tools/jEdit/src/jedit_resources.scala --- 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() } } diff -r 1c083e32aed6 -r 186dcfe746e3 src/Tools/jEdit/src/main_plugin.scala --- 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 } }