src/Pure/PIDE/headless.scala

--- a/src/Pure/PIDE/headless.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -91,7 +91,7 @@
       def finished: Load_State = Load_State(Nil, Nil, Space.zero)
 
       def count_file(name: Document.Node.Name): Long =
-        if (resources.session_base.loaded_theory(name)) 0 else File.size(name.path)
+        if (resources.loaded_theory(name)) 0 else File.size(name.path)
     }
 
     private case class Load_State(
@@ -206,7 +206,7 @@
         version: Document.Version,
         name: Document.Node.Name
       ): Boolean = {
-        resources.session_base.loaded_theory(name) ||
+        resources.loaded_theory(name) ||
         nodes_status.quasi_consolidated(name) ||
         (if (commit.isDefined) already_committed.isDefinedAt(name)
          else state.node_consolidated(version, name))
@@ -226,7 +226,7 @@
                   case (committed, name) =>
                     def parents_committed: Boolean =
                       version.nodes(name).header.imports.forall(parent =>
-                        resources.session_base.loaded_theory(parent) || committed.isDefinedAt(parent))
+                        resources.loaded_theory(parent) || committed.isDefinedAt(parent))
                     if (!committed.isDefinedAt(name) && parents_committed &&
                         state.node_consolidated(version, name)) {
                       val snapshot = stable_snapshot(state, version, name)
@@ -239,7 +239,7 @@
           }
 
         def committed(name: Document.Node.Name): Boolean =
-          resources.session_base.loaded_theory(name) || st1.already_committed.isDefinedAt(name)
+          resources.loaded_theory(name) || st1.already_committed.isDefinedAt(name)
 
         val (load_theories0, load_state1) =
           load_state.next(dep_graph, consolidated(state, version, _))
@@ -257,7 +257,7 @@
             ): Option[List[(Document.Node.Name, Document_Status.Node_Status)]] = {
               input match {
                 case name :: rest =>
-                  if (resources.session_base.loaded_theory(name)) make_nodes(rest, output)
+                  if (resources.loaded_theory(name)) make_nodes(rest, output)
                   else {
                     val status = Document_Status.Node_Status.make(state, version, name)
                     val ok = if (commit.isDefined) committed(name) else status.consolidated