# HG changeset patch
# User wenzelm
# Date 1659179179 -7200
# Node ID 5d84eec431142f1921f3e658459e2480d47b7913
# Parent  642ecd97d35c2452a5292ae0d6f7b4f5dc828b72
clarified names;

diff -r 642ecd97d35c -r 5d84eec43114 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Jul 30 11:35:04 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Jul 30 13:06:19 2022 +0200
@@ -32,7 +32,7 @@
     def files_path(name: Document.Node.Name, path: Path): Path =
       theory_dir(name) + Path.explode("files") + path.squash.html
 
-    def theory_exports: Theory_Exports = Theory_Exports.empty
+    def nodes: Nodes = Nodes.empty
 
 
     /* HTML content */
@@ -85,19 +85,19 @@
       language = Markup.Elements(Markup.Language.DOCUMENT))
 
 
-  /* theory exports */
+  /* per-session node info */
 
-  object Theory_Export {
-    val empty: Theory_Export = new Theory_Export(Map.empty, Map.empty, Nil)
-    def make(theory: Export_Theory.Theory): Theory_Export = {
+  object Node_Info {
+    val empty: Node_Info = new Node_Info(Map.empty, Map.empty, Nil)
+    def make(theory: Export_Theory.Theory): Node_Info = {
       val by_range = theory.entity_iterator.toList.groupBy(_.range)
       val by_kind_name =
         theory.entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap
       val others = theory.others.keySet.toList
-      new Theory_Export(by_range, by_kind_name, others)
+      new Node_Info(by_range, by_kind_name, others)
     }
   }
-  class Theory_Export private(
+  class Node_Info private(
     by_range: Map[Symbol.Range, List[Export_Theory.Entity0]],
     by_kind_name: Map[(String, String), Export_Theory.Entity0],
     val others: List[String]) {
@@ -107,14 +107,13 @@
       by_kind_name.get((kind, name)).map(_.kname)
   }
 
-  object Theory_Exports {
-    val empty: Theory_Exports = make(Nil)
-    def make(entries: Iterable[(String, Theory_Export)]): Theory_Exports =
-      new Theory_Exports(entries.toMap)
+  object Nodes {
+    val empty: Nodes = make(Nil)
+    def make(infos: Iterable[(String, Node_Info)]): Nodes = new Nodes(infos.toMap)
   }
-  class Theory_Exports private(export_by_session: Map[String, Theory_Export]) {
-    def apply(name: String): Theory_Export = export_by_session.getOrElse(name, Theory_Export.empty)
-    def get(name: String): Option[Theory_Export] = export_by_session.get(name)
+  class Nodes private(by_session: Map[String, Node_Info]) {
+    def apply(name: String): Node_Info = by_session.getOrElse(name, Node_Info.empty)
+    def get(name: String): Option[Node_Info] = by_session.get(name)
   }
 
 
@@ -158,7 +157,7 @@
             case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
             case _ =>
               Some {
-                val entities = html_context.theory_exports(node.theory).for_range(range)
+                val entities = html_context.nodes(node.theory).for_range(range)
                 val body1 =
                   if (seen_ranges.contains(range)) {
                     HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
@@ -185,7 +184,7 @@
         }
 
         private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
-          html_context.theory_exports.get(thy_name).flatMap(_.get_kind_name(kind, name))
+          html_context.nodes.get(thy_name).flatMap(_.get_kind_name(kind, name))
 
         override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = {
           props match {
@@ -473,11 +472,11 @@
     session_relative(deps, session0, session1)
   }
 
-  def read_exports(
+  def read_nodes(
     sessions: List[String],
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context
-  ): Theory_Exports = {
+  ): Nodes = {
     type Batch = (String, List[String])
     val batches =
       sessions.foldLeft((Set.empty[String], List.empty[Batch]))(
@@ -485,8 +484,8 @@
             val thys = deps(session).loaded_theories.keys.filterNot(seen)
             (seen ++ thys, (session, thys) :: batches)
         })._2
-    val exports =
-      Par_List.map[Batch, List[(String, Theory_Export)]](
+    val infos =
+      Par_List.map[Batch, List[(String, Node_Info)]](
         { case (session, thys) =>
             for (thy_name <- thys) yield {
               val theory =
@@ -498,10 +497,10 @@
                   }
                   else Export_Theory.no_theory
                 }
-              thy_name -> Theory_Export.make(theory)
+              thy_name -> Node_Info.make(theory)
             }
         }, batches).flatten
-    Theory_Exports.make(exports)
+    Nodes.make(infos)
   }
 
   def session_html(
@@ -581,8 +580,7 @@
 
         val thy_elements =
           session_elements.copy(entity =
-            html_context.theory_exports(name.theory).others
-              .foldLeft(session_elements.entity)(_ + _))
+            html_context.nodes(name.theory).others.foldLeft(session_elements.entity)(_ + _))
 
         val files_html =
           for {
diff -r 642ecd97d35c -r 5d84eec43114 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 30 11:35:04 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 30 13:06:19 2022 +0200
@@ -495,8 +495,8 @@
         }
 
         using(store.open_database_context()) { db_context =>
-          val exports =
-            Presentation.read_exports(presentation_sessions.map(_.name), deps, db_context)
+          val presentation_nodes =
+            Presentation.read_nodes(presentation_sessions.map(_.name), deps, db_context)
 
           Par_List.map({ (session: String) =>
             progress.expose_interrupt()
@@ -507,7 +507,7 @@
                 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))
-                override def theory_exports: Presentation.Theory_Exports = exports
+                override def nodes: Presentation.Nodes = presentation_nodes
               }
             Presentation.session_html(
               session, deps, db_context, progress = progress,