src/Pure/Thy/export.scala

 
     def session_name: String =
       if (document_snapshot.isDefined) Sessions.DRAFT
       else session_base.session_name
 
+    def session_database(session: String = session_name): Option[Session_Database] =
+      db_hierarchy.find(_.session == session)
+
+    def session_db(session: String = session_name): Option[SQL.Database] =
+      session_database(session = session).map(_.db)
+
     def session_stack: List[String] =
       ((if (document_snapshot.isDefined) List(session_name) else Nil) :::
         db_hierarchy.map(_.session)).reverse
 
     private def select[A](

             snapshot <- document_snapshot.iterator
             entry_name <- snapshot.all_exports.keysIterator
             res <- select1(entry_name).iterator
           } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
         }
-        else { db_hierarchy.find(_.session == name).map(select2).getOrElse(Nil) }
+        else { session_database(name).map(select2).getOrElse(Nil) }
       if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
     }
 
     def entry_names(session: String = session_name): List[Entry_Name] =
       select(session, Some(_), _.entry_names)

         case Some(entry) => entry
       }
 
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)
-
-    def read_document(session: String, name: String): Option[Document_Build.Document_Output] =
-      db_hierarchy.find(_.session == session).flatMap(session_db =>
-        Document_Build.read_document(session_db.db, session_db.session, name))
 
     override def toString: String =
       "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }