# HG changeset patch
# User wenzelm
# Date 1526568133 -7200
# Node ID 9a8949f71fd4a941501f4ab6ffc127627fef1fe9
# Parent  a554da2811f2b5e3b1b123ac2d555a2473df3d35
tuned signature;

diff -r a554da2811f2 -r 9a8949f71fd4 src/Pure/Thy/export.scala
--- 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)
diff -r a554da2811f2 -r 9a8949f71fd4 src/Pure/Thy/sessions.scala
--- 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" +