# HG changeset patch
# User wenzelm
# Date 1670413086 -3600
# Node ID 3fc3c7c285cdc71428d6d3597d76dbd3fd8e66dd
# Parent  6cd6c553b48094b3b47967323e173d193ac98d77
clarified signature;

diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Pure/PIDE/resources.scala
--- 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
diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Pure/PIDE/session.scala
--- 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) {
diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Tools/VSCode/src/language_server.scala
--- 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
diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Tools/VSCode/src/vscode_resources.scala
--- 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 {
diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Tools/jEdit/src/jedit_resources.scala
--- 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()
   }
 }
diff -r 6cd6c553b480 -r 3fc3c7c285cd src/Tools/jEdit/src/main_plugin.scala
--- 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
           }
         }