# HG changeset patch
# User wenzelm
# Date 1605987348 -3600
# Node ID e0443773ef1a4bab60459243710d6468eaa053b8
# Parent  035b8054013a0c0adaadcc5b10e0e7c8630aa7a3
clarified modules;

diff -r 035b8054013a -r e0443773ef1a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Nov 21 19:48:05 2020 +0100
+++ b/src/Pure/Thy/export.scala	Sat Nov 21 20:35:48 2020 +0100
@@ -185,55 +185,6 @@
   }
 
 
-  /* database context */
-
-  def open_database_context(
-    sessions_structure: Sessions.Structure,
-    store: Sessions.Store): Database_Context =
-  {
-    new Database_Context(sessions_structure, store,
-      if (store.database_server) Some(store.open_database_server()) else None)
-  }
-
-  class Database_Context private[Export](
-    sessions_structure: Sessions.Structure,
-    store: Sessions.Store,
-    database_server: Option[SQL.Database]) extends AutoCloseable
-  {
-    def close { database_server.foreach(_.close) }
-
-    def try_entry(session: String, theory_name: String, name: String): Option[Entry] =
-    {
-      val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
-      val attempts =
-        database_server match {
-          case Some(db) =>
-            hierarchy.map(session_name => read_entry(db, session_name, theory_name, name))
-          case None =>
-            hierarchy.map(session_name =>
-              store.try_open_database(session_name) match {
-                case Some(db) => using(db)(read_entry(_, session_name, theory_name, name))
-                case None => None
-              })
-        }
-      attempts.collectFirst({ case Some(entry) => entry })
-    }
-
-    def entry(session: String, theory_name: String, name: String): Entry =
-      try_entry(session, theory_name, name) getOrElse empty_entry(session, theory_name, name)
-
-    override def toString: String =
-    {
-      val s =
-        database_server match {
-          case Some(db) => db.toString
-          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
-        }
-      "Database_Context(" + s + ")"
-    }
-  }
-
-
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
@@ -290,10 +241,10 @@
       }
 
     def database_context(
-        context: Database_Context, session: String, theory_name: String): Provider =
+        context: Sessions.Database_Context, session: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
-          context.try_entry(session, theory_name, export_name)
+          context.try_export(session, theory_name, export_name)
 
         def focus(other_theory: String): Provider = this
 
diff -r 035b8054013a -r e0443773ef1a src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 21 19:48:05 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 21 20:35:48 2020 +0100
@@ -335,6 +335,7 @@
   }
 
 
+
   /** preview **/
 
   sealed case class Preview(title: String, content: String)
@@ -455,10 +456,10 @@
     /* prepare document directory */
 
     lazy val tex_files =
-      using(Export.open_database_context(deps.sessions_structure, store))(context =>
+      using(store.open_database_context(deps.sessions_structure))(context =>
         for (name <- base.session_theories ::: base.document_theories)
         yield {
-          val entry = context.entry(session, name.theory, document_tex_name(name))
+          val entry = context.export(session, name.theory, document_tex_name(name))
           Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
         }
       )
diff -r 035b8054013a -r e0443773ef1a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Nov 21 19:48:05 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Nov 21 20:35:48 2020 +0100
@@ -1180,6 +1180,45 @@
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
 
+  class Database_Context private[Sessions](
+    val store: Sessions.Store,
+    sessions_structure: Sessions.Structure,
+    database_server: Option[SQL.Database]) extends AutoCloseable
+  {
+    def close { database_server.foreach(_.close) }
+
+    def try_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
+    {
+      val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
+      val attempts =
+        database_server match {
+          case Some(db) =>
+            hierarchy.map(session_name => Export.read_entry(db, session_name, theory_name, name))
+          case None =>
+            hierarchy.map(session_name =>
+              store.try_open_database(session_name) match {
+                case Some(db) => using(db)(Export.read_entry(_, session_name, theory_name, name))
+                case None => None
+              })
+        }
+      attempts.collectFirst({ case Some(entry) => entry })
+    }
+
+    def export(session: String, theory_name: String, name: String): Export.Entry =
+      try_export(session, theory_name, name) getOrElse
+        Export.empty_entry(session, theory_name, name)
+
+    override def toString: String =
+    {
+      val s =
+        database_server match {
+          case Some(db) => db.toString
+          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
+        }
+      "Database_Context(" + s + ")"
+    }
+  }
+
   def store(options: Options): Store = new Store(options)
 
   class Store private[Sessions](val options: Options)
@@ -1259,6 +1298,10 @@
               port = options.int("build_database_ssh_port"))),
         ssh_close = true)
 
+    def open_database_context(sessions_structure: Sessions.Structure): Database_Context =
+      new Database_Context(store, sessions_structure,
+        if (database_server) Some(open_database_server()) else None)
+
     def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
       def check(db: SQL.Database): Option[SQL.Database] =