# HG changeset patch
# User wenzelm
# Date 1659182281 -7200
# Node ID 6f46853dbec4879d2f1191a5757d3802028e28b1
# Parent  20a03e16d8fae382775df5935402691e7c30f8a1
clarified signature;

diff -r 20a03e16d8fa -r 6f46853dbec4 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Jul 30 13:53:15 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Jul 30 13:58:01 2022 +0200
@@ -107,8 +107,37 @@
   }
 
   object Nodes {
-    val empty: Nodes = make(Nil)
-    def make(infos: Iterable[(String, Node_Info)]): Nodes = new Nodes(infos.toMap)
+    val empty: Nodes = new Nodes(Map.empty)
+    def read(
+      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]))(
+          { case ((seen, batches), session) =>
+              val thys = deps(session).loaded_theories.keys.filterNot(seen)
+              (seen ++ thys, (session, thys) :: batches)
+          })._2
+      val theory_node_info =
+        Par_List.map[Batch, List[(String, Node_Info)]](
+          { case (session, thys) =>
+              for (thy_name <- thys) yield {
+                val theory =
+                  if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
+                  else {
+                    val provider = Export.Provider.database_context(db_context, List(session), thy_name)
+                    if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
+                      Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache)
+                    }
+                    else Export_Theory.no_theory
+                  }
+                thy_name -> Node_Info.make(theory)
+              }
+          }, batches).flatten.toMap
+      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)
@@ -471,37 +500,6 @@
     session_relative(deps, session0, session1)
   }
 
-  def read_nodes(
-    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]))(
-        { case ((seen, batches), session) =>
-            val thys = deps(session).loaded_theories.keys.filterNot(seen)
-            (seen ++ thys, (session, thys) :: batches)
-        })._2
-    val infos =
-      Par_List.map[Batch, List[(String, Node_Info)]](
-        { case (session, thys) =>
-            for (thy_name <- thys) yield {
-              val theory =
-                if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
-                else {
-                  val provider = Export.Provider.database_context(db_context, List(session), thy_name)
-                  if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
-                    Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache)
-                  }
-                  else Export_Theory.no_theory
-                }
-              thy_name -> Node_Info.make(theory)
-            }
-        }, batches).flatten
-    Nodes.make(infos)
-  }
-
   def session_html(
     session: String,
     deps: Sessions.Deps,
diff -r 20a03e16d8fa -r 6f46853dbec4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 30 13:53:15 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 30 13:58:01 2022 +0200
@@ -496,7 +496,7 @@
 
         using(store.open_database_context()) { db_context =>
           val presentation_nodes =
-            Presentation.read_nodes(presentation_sessions.map(_.name), deps, db_context)
+            Presentation.Nodes.read(presentation_sessions.map(_.name), deps, db_context)
 
           Par_List.map({ (session: String) =>
             progress.expose_interrupt()