# HG changeset patch
# User wenzelm
# Date 1659799739 -7200
# Node ID 0e5339342998edb42dfbf2e8a8f0a2e00b34e640
# Parent  f49c4f160b8423e052dedcab3961ceb9845e172d
clarified signature: prefer Export.Context;

diff -r f49c4f160b84 -r 0e5339342998 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 06 17:16:19 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 06 17:28:59 2022 +0200
@@ -113,11 +113,13 @@
     val empty: Nodes = new Nodes(Map.empty, Map.empty)
 
     def read(
-      presentation_sessions: List[String],
+      export_context: Export.Context,
       deps: Sessions.Deps,
-      db_context: Sessions.Database_Context
+      presentation_sessions: List[String]
     ): Nodes = {
-      val export_context = Export.context(db_context)
+
+      def open_session(session: String): Export.Session_Context =
+        export_context.open_session(deps.base_info(session))
 
       type Batch = (String, List[String])
       val batches =
@@ -130,12 +132,12 @@
       val theory_node_info =
         Par_List.map[Batch, List[(String, Node_Info)]](
           { case (session, thys) =>
-              using(export_context.open_session(deps.base_info(session))) { session_context =>
+              using(open_session(session)) { session_context =>
                 for (thy_name <- thys) yield {
                   val theory_context = session_context.theory(thy_name)
                   val theory =
                     Export_Theory.read_theory(theory_context,
-                      permissive = true, cache = db_context.cache)
+                      permissive = true, cache = session_context.cache)
                   thy_name -> Node_Info.make(theory)
                 }
               }
@@ -143,10 +145,9 @@
 
       val files_info =
         deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session =>
-          using(export_context.open_session(deps.base_info(session))) { session_context =>
+          using(open_session(session)) { session_context =>
             session_context.theory_names().flatMap { theory =>
-              val theory_context = session_context.theory(theory)
-              theory_context.files() match {
+              session_context.theory(theory).files() match {
                 case None => Nil
                 case Some((thy, blobs)) =>
                   val thy_file_info = File_Info(theory, is_theory = true)
diff -r f49c4f160b84 -r 0e5339342998 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Aug 06 17:16:19 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sat Aug 06 17:28:59 2022 +0200
@@ -495,10 +495,8 @@
         }
 
         using(Export.open_context(store)) { export_context =>
-          val db_context = export_context.db_context
-
           val presentation_nodes =
-            Presentation.Nodes.read(presentation_sessions.map(_.name), deps, db_context)
+            Presentation.Nodes.read(export_context, deps, presentation_sessions.map(_.name))
 
           Par_List.map({ (session: String) =>
             progress.expose_interrupt()
@@ -512,8 +510,7 @@
                   deps.sessions_structure(deps(session).theory_qualifier(name))
               }
 
-            val session_base_info = deps.base_info(session)
-            using(export_context.open_session(session_base_info)) { session_context =>
+            using(export_context.open_session(deps.base_info(session))) { session_context =>
               Presentation.session_html(session_context, deps,
                 progress = progress,
                 verbose = verbose,