tuned;
authorwenzelm
Sat, 30 Jul 2022 14:00:03 +0200
changeset 75731 5d225d786177
parent 75730 6f46853dbec4
child 75732 14598eca6c20
tuned;
src/Pure/Thy/presentation.scala
src/Pure/Tools/build.scala
--- a/src/Pure/Thy/presentation.scala	Sat Jul 30 13:58:01 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Jul 30 14:00:03 2022 +0200
@@ -96,6 +96,7 @@
       new Node_Info(by_range, by_kind_name, others)
     }
   }
+
   class Node_Info private(
     by_range: Map[Symbol.Range, List[Export_Theory.Entity0]],
     by_kind_name: Map[(String, String), Export_Theory.Entity0],
@@ -108,14 +109,15 @@
 
   object Nodes {
     val empty: Nodes = new Nodes(Map.empty)
+
     def read(
-      sessions: List[String],
+      presentation_sessions: List[String],
       deps: Sessions.Deps,
       db_context: Sessions.Database_Context
     ): Nodes = {
       type Batch = (String, List[String])
       val batches =
-        sessions.foldLeft((Set.empty[String], List.empty[Batch]))(
+        presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))(
           { case ((seen, batches), session) =>
               val thys = deps(session).loaded_theories.keys.filterNot(seen)
               (seen ++ thys, (session, thys) :: batches)
@@ -139,6 +141,7 @@
       new Nodes(theory_node_info)
     }
   }
+
   class Nodes private(theory_node_info: Map[String, Node_Info]) {
     def apply(name: String): Node_Info = theory_node_info.getOrElse(name, Node_Info.empty)
     def get(name: String): Option[Node_Info] = theory_node_info.get(name)
--- a/src/Pure/Tools/build.scala	Sat Jul 30 13:58:01 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 30 14:00:03 2022 +0200
@@ -504,10 +504,10 @@
 
             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))
-                override def nodes: Presentation.Nodes = presentation_nodes
               }
             Presentation.session_html(
               session, deps, db_context, progress = progress,