--- a/src/Pure/Thy/export.scala Thu May 17 15:38:36 2018 +0200
+++ b/src/Pure/Thy/export.scala Thu May 17 16:42:13 2018 +0200
@@ -253,13 +253,8 @@
/* database */
val store = Sessions.store(system_mode)
- val database =
- store.find_database(session_name) match {
- case None => error("Missing database for session " + quote(session_name))
- case Some(database) => database
- }
- using(SQLite.open_database(database))(db =>
+ using(SQLite.open_database(store.the_database(session_name)))(db =>
{
db.transaction {
val export_names = read_theory_names(db, session_name)
--- a/src/Pure/Thy/sessions.scala Thu May 17 15:38:36 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Thu May 17 16:42:13 2018 +0200
@@ -1025,6 +1025,9 @@
def find_database(name: String): Option[Path] =
input_dirs.map(_ + database(name)).find(_.is_file)
+ def the_database(name: String): Path =
+ find_database(name) getOrElse error("Missing database for session " + quote(name))
+
def heap(name: String): Path =
input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +