# HG changeset patch
# User wenzelm
# Date 1753711802 -7200
# Node ID af85ea5d9b20b6f50a89824a31726bcda9844c6a
# Parent  b7678301588ca558476e58ae95c43bb57bfa6402
tuned signature;

diff -r b7678301588c -r af85ea5d9b20 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Mon Jul 28 15:58:40 2025 +0200
+++ b/src/Pure/Build/resources.scala	Mon Jul 28 16:10:02 2025 +0200
@@ -32,6 +32,9 @@
   def sessions_structure: Sessions.Structure = session_background.sessions_structure
   def session_base: Sessions.Base = session_background.base
 
+  def loaded_theory(name: String): Boolean = session_base.loaded_theory(name)
+  def loaded_theory(name: Document.Node.Name): Boolean = session_base.loaded_theory(name)
+
   override def toString: String = "Resources(" + session_base.print_body + ")"
 
 
@@ -144,7 +147,7 @@
     if (literal_import && !Url.is_base_name(s)) {
       error("Bad import of theory from other session via file-path: " + quote(s))
     }
-    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+    if (loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
@@ -236,7 +239,7 @@
   def undefined_blobs(version: Document.Version): List[Document.Node.Name] =
     (for {
       (node_name, node) <- version.nodes.iterator
-      if !session_base.loaded_theory(node_name)
+      if !loaded_theory(node_name)
       cmd <- node.load_commands.iterator
       name <- cmd.blobs_undefined.iterator
     } yield name).toList
@@ -295,7 +298,7 @@
       if (seen.isDefinedAt(name)) this
       else {
         val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
-        if (session_base.loaded_theory(name)) dependencies1
+        if (loaded_theory(name)) dependencies1
         else {
           try {
             if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
diff -r b7678301588c -r af85ea5d9b20 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jul 28 15:58:40 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jul 28 16:10:02 2025 +0200
@@ -862,7 +862,7 @@
           case None =>
             List(
               Node.Deps(
-                if (session.resources.session_base.loaded_theory(node_name)) {
+                if (session.resources.loaded_theory(node_name)) {
                   node_header.append_errors(
                     List("Cannot update finished theory " + quote(node_name.theory)))
                 }
diff -r b7678301588c -r af85ea5d9b20 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Mon Jul 28 15:58:40 2025 +0200
+++ b/src/Pure/PIDE/document_editor.scala	Mon Jul 28 16:10:02 2025 +0200
@@ -141,7 +141,7 @@
         else {
           val snapshot = pide_session.snapshot()
           def document_ready(theory: String): Boolean =
-            pide_session.resources.session_base.loaded_theory(theory) ||
+            pide_session.resources.loaded_theory(theory) ||
             snapshot.theory_consolidated(theory)
           if (snapshot.is_outdated || !selection.forall(document_ready)) None
           else Some(snapshot)
diff -r b7678301588c -r af85ea5d9b20 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Mon Jul 28 15:58:40 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Jul 28 16:10:02 2025 +0200
@@ -275,7 +275,7 @@
       val update_iterator =
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
-          if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name)
+          if !Resources.hidden_node(name) && !resources.loaded_theory(name)
           st = Document_Status.Node_Status.make(state, version, name)
           if !rep.isDefinedAt(name) || rep(name) != st
         } yield (name -> st)
diff -r b7678301588c -r af85ea5d9b20 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jul 28 15:58:40 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jul 28 16:10:02 2025 +0200
@@ -97,7 +97,7 @@
     find_theory(file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+      if (loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else Document.Node.Name(node, theory = theory)
     }