tuned signature;

--- 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

--- a/src/Pure/PIDE/session.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -672,7 +672,7 @@
                 case Some(version) =>
                   val consolidate =
                     version.nodes.descendants(consolidation.flush().toList).filter { name =>
-                      !resources.session_base.loaded_theory(name) &&
+                      !resources.loaded_theory(name) &&
                       !state.node_consolidated(version, name) &&
                       state.node_maybe_consolidated(version, name)
                     }

--- a/src/Pure/Tools/dump.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -232,7 +232,7 @@
         session_name <-
           deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
         (name, theory_options) <- deps(session_name).used_theories
-        if !resources.session_base.loaded_theory(name)
+        if !resources.loaded_theory(name)
         if {
           def warn(msg: String): Unit =
             progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")

--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -34,7 +34,7 @@
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       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)
     }
 

--- a/src/Tools/jEdit/src/theories_status.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -26,7 +26,7 @@
   private var document_required = Set.empty[Document.Node.Name]
 
   private def is_loaded_theory(name: Document.Node.Name): Boolean =
-    PIDE.resources.session_base.loaded_theory(name)
+    PIDE.resources.loaded_theory(name)
 
   private def overall_node_status(name: Document.Node.Name): Document_Status.Overall_Node_Status = {
     if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok

--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Jul 28 16:11:12 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Jul 28 16:14:46 2025 +0200
@@ -169,7 +169,7 @@
         case None => snapshot.version.nodes.iterator
       }).foldLeft(nodes_timing) {
           case (timing1, (name, node)) =>
-            if (PIDE.resources.session_base.loaded_theory(name)) timing1
+            if (PIDE.resources.loaded_theory(name)) timing1
             else {
               val node_timing =
                 Document_Status.Overall_Timing.make(