--- a/src/Pure/PIDE/resources.scala Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Wed Dec 07 12:38:06 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 Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Pure/PIDE/session.scala Wed Dec 07 12:38:06 2022 +0100
@@ -690,6 +690,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/Tools/VSCode/src/language_server.scala Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Wed Dec 07 12:38:06 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 Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Dec 07 12:38:06 2022 +0100
@@ -210,17 +210,8 @@
state.change_result { st =>
val thy_files = resources.resolve_dependencies(st.models, Nil)
- 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 stable_tip_version = session.stable_tip_version(st.models)
+ val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
val loaded_models =
(for {
--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 07 12:38:06 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 Tue Dec 06 20:08:51 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Wed Dec 07 12:38:06 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
}
}