# HG changeset patch
# User wenzelm
# Date 1606390029 -3600
# Node ID 7cef6b1a6682e9cd2760df043fa6a3f8c0f5716d
# Parent  2615b8c053373488bcea22903966441910f7d3e1
clarified signature;

diff -r 2615b8c05337 -r 7cef6b1a6682 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 26 12:21:45 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 26 12:27:09 2020 +0100
@@ -266,7 +266,7 @@
     val documents =
       for {
         doc <- info.document_variants
-        document <- db_context.read_document(session, doc.name)
+        document <- db_context.input_database(session)(read_document(_, _, doc.name))
       } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
 
     val links =
@@ -533,7 +533,7 @@
 
           val old_document =
             for {
-              old_doc <- db_context.read_document(session, doc.name)
+              old_doc <- db_context.input_database(session)(read_document(_, _, doc.name))
               if old_doc.sources == sources
             }
             yield {
diff -r 2615b8c05337 -r 7cef6b1a6682 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Nov 26 12:21:45 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Nov 26 12:27:09 2020 +0100
@@ -1196,6 +1196,16 @@
         case None => using(store.open_database(session, output = true))(f)
       }
 
+    def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] =
+      database_server match {
+        case Some(db) => f(db, session)
+        case None =>
+          store.try_open_database(session) match {
+            case Some(db) => using(db)(f(_, session))
+            case None => None
+          }
+      }
+
     def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
     {
       val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
@@ -1217,16 +1227,6 @@
       read_export(session, theory_name, name) getOrElse
         Export.empty_entry(session, theory_name, name)
 
-    def read_document(session_name: String, name: String): Option[Presentation.Document_Output] =
-      database_server match {
-        case Some(db) => Presentation.read_document(db, session_name, name)
-        case None =>
-          store.try_open_database(session_name) match {
-            case Some(db) => using(db)(Presentation.read_document(_, session_name, name))
-            case None => None
-          }
-      }
-
     override def toString: String =
     {
       val s =