--- 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 =