clarified signature: avoid object-oriented HTML_Context;
clarified theory_qualifier --- belongs to the overall Sessions.Structure;

--- a/src/Pure/PIDE/resources.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -157,7 +157,7 @@
 
   def find_theory_node(theory: String): Option[Document.Node.Name] = {
     val thy_file = Path.basic(Long_Name.base_name(theory)).thy
-    val session = session_base.theory_qualifier(theory)
+    val session = sessions_structure.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
         case Some(info) => info.dirs
@@ -182,7 +182,7 @@
   }
 
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
-    import_name(session_base.theory_qualifier(name), name.master_dir, s)
+    import_name(sessions_structure.theory_qualifier(name), name.master_dir, s)
 
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
@@ -198,7 +198,7 @@
   }
 
   def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = {
-    val context_session = session_base.theory_qualifier(context_name)
+    val context_session = sessions_structure.theory_qualifier(context_name)
     val context_dir =
       try { Some(context_name.master_dir_path) }
       catch { case ERROR(_) => None }

--- a/src/Pure/Thy/presentation.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -17,19 +17,26 @@
 
   /* HTML context */
 
-  sealed case class HTML_Document(title: String, content: String)
+  def html_context(
+    sessions_structure: Sessions.Structure,
+    root_dir: Path = Path.current,
+    nodes: Nodes = Nodes.empty
+  ): HTML_Context = new HTML_Context(sessions_structure, root_dir, nodes)
 
-  abstract class HTML_Context {
+  class HTML_Context private[Presentation](
+    sessions_structure: Sessions.Structure,
+    val root_dir: Path,
+    val nodes: Nodes
+  ) {
     /* directory structure and resources */
 
-    def nodes: Nodes
-    def root_dir: Path
-    def theory_session(name: Document.Node.Name): Sessions.Info
+    def theory_session_info(name: Document.Node.Name): Sessions.Info =
+      sessions_structure(sessions_structure.theory_qualifier(name))
 
     def session_dir(info: Sessions.Info): Path =
       root_dir + Path.explode(info.chapter_session)
     def theory_dir(name: Document.Node.Name): Path =
-      session_dir(theory_session(name))
+      session_dir(theory_session_info(name))
     def files_path(name: Document.Node.Name, path: Path): Path =
       theory_dir(name) + Path.explode("files") + path.squash.html
 
@@ -63,6 +70,8 @@
     }
   }
 
+  sealed case class HTML_Document(title: String, content: String)
+
 
   /* presentation elements */
 
@@ -518,7 +527,7 @@
     session0: String,
     node_name: Document.Node.Name
   ): Option[String] = {
-    val session1 = deps(session0).theory_qualifier(node_name)
+    val session1 = deps.sessions_structure.theory_qualifier(node_name)
     session_relative(deps, session0, session1)
   }
 
@@ -619,7 +628,7 @@
             make_html(entity_context(name), thy_elements,
               snapshot.xml_markup(elements = thy_elements.html)))
 
-        val thy_session = html_context.theory_session(name).name
+        val thy_session = html_context.theory_session_info(name).name
         val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name))
         val files =
           for { (src_path, file_html) <- files_html }

--- a/src/Pure/Thy/sessions.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -81,10 +81,6 @@
         ", loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
-    def theory_qualifier(name: String): String =
-      global_theories.getOrElse(name, Long_Name.qualifier(name))
-    def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
-
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
@@ -183,7 +179,8 @@
             val overall_syntax = dependencies.overall_syntax
 
             val proper_session_theories =
-              dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
+              dependencies.theories.filter(name =>
+                sessions_structure.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
 
@@ -213,7 +210,7 @@
                 Graph_Display.Node("[" + name + "]", "session." + name)
 
               def node(name: Document.Node.Name): Graph_Display.Node = {
-                val qualifier = deps_base.theory_qualifier(name)
+                val qualifier = sessions_structure.theory_qualifier(name)
                 if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
@@ -221,7 +218,7 @@
 
               val required_sessions =
                 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
-                  .map(theory => deps_base.theory_qualifier(theory))
+                  .map(theory => sessions_structure.theory_qualifier(theory))
                   .filter(name => name != info.name && sessions_structure.defined(name))
 
               val required_subgraph =
@@ -258,7 +255,7 @@
                 sessions_structure.imports_requirements(List(session_name)).toSet
               for {
                 name <- dependencies.theories
-                qualifier = deps_base.theory_qualifier(name)
+                qualifier = sessions_structure.theory_qualifier(name)
                 if !known_sessions(qualifier)
               } yield "Bad import of theory " + quote(name.toString) +
                 ": need to include sessions " + quote(qualifier) + " in ROOT"
@@ -280,7 +277,7 @@
                   known_theories.get(thy).map(_.name) match {
                     case None => err("Unknown document theory")
                     case Some(name) =>
-                      val qualifier = deps_base.theory_qualifier(name)
+                      val qualifier = sessions_structure.theory_qualifier(name)
                       if (proper_session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
@@ -413,7 +410,7 @@
         val required_theories =
           for {
             thy <- base.loaded_theories.keys
-            if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
+            if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session
           }
           yield thy
 
@@ -764,6 +761,7 @@
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
+    def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
 
     def check_sessions(names: List[String]): Unit = {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList

--- a/src/Pure/Tools/build.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Pure/Tools/build.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -504,12 +504,10 @@
             progress.echo("Presenting " + session + " ...")
 
             val html_context =
-              new Presentation.HTML_Context {
-                override def nodes: Presentation.Nodes = presentation_nodes
-                override def root_dir: Path = presentation_dir
-                override def theory_session(name: Document.Node.Name): Sessions.Info =
-                  deps.sessions_structure(deps(session).theory_qualifier(name))
-              }
+              Presentation.html_context(
+                sessions_structure = deps.sessions_structure,
+                root_dir = presentation_dir,
+                nodes = presentation_nodes)
 
             using(database_context.open_session(deps.base_info(session))) { session_context =>
               Presentation.session_html(session_context, deps,

--- a/src/Tools/VSCode/src/preview_panel.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -28,13 +28,7 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val html_context =
-                    new Presentation.HTML_Context {
-                      override def nodes: Presentation.Nodes = Presentation.Nodes.empty
-                      override def root_dir: Path = Path.current
-                      override def theory_session(name: Document.Node.Name): Sessions.Info =
-                        resources.sessions_structure(resources.session_base.theory_qualifier(name))
-                    }
+                  val html_context = Presentation.html_context(resources.sessions_structure)
                   val document =
                     Presentation.html_document(snapshot, html_context, Presentation.elements2)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))

--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -313,14 +313,7 @@
       }
       yield {
         val snapshot = model.await_stable_snapshot()
-        val html_context =
-          new Presentation.HTML_Context {
-            override def nodes: Presentation.Nodes = Presentation.Nodes.empty
-            override def root_dir: Path = Path.current
-            override def theory_session(name: Document.Node.Name): Sessions.Info =
-              PIDE.resources.sessions_structure(
-                PIDE.resources.session_base.theory_qualifier(name))
-          }
+        val html_context = Presentation.html_context(PIDE.resources.sessions_structure)
         val document =
           Presentation.html_document(
             snapshot, html_context, Presentation.elements2,

--- a/src/Tools/jEdit/src/isabelle_session.scala	Wed Aug 17 11:57:13 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala	Wed Aug 17 14:42:20 2022 +0200
@@ -84,10 +84,10 @@
       PIDE.maybe_snapshot(view) match {
         case None => ""
         case Some(snapshot) =>
-          val sessions = JEdit_Sessions.sessions_structure()
-          val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
+          val sessions_structure = JEdit_Sessions.sessions_structure()
+          val session = sessions_structure.theory_qualifier(snapshot.node_name)
           val chapter =
-            sessions.get(session) match {
+            sessions_structure.get(session) match {
               case Some(info) => info.chapter
               case None => Sessions.UNSORTED
             }