tuned signature;
authorwenzelm
Thu May 17 16:42:13 2018 +0200 (4 days ago)
changeset 682059a8949f71fd4
parent 68204 a554da2811f2
child 68206 dedf1a70d1fa
tuned signature;
src/Pure/Thy/export.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/export.scala	Thu May 17 15:38:36 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Thu May 17 16:42:13 2018 +0200
     1.3 @@ -253,13 +253,8 @@
     1.4      /* database */
     1.5  
     1.6      val store = Sessions.store(system_mode)
     1.7 -    val database =
     1.8 -      store.find_database(session_name) match {
     1.9 -        case None => error("Missing database for session " + quote(session_name))
    1.10 -        case Some(database) => database
    1.11 -      }
    1.12  
    1.13 -    using(SQLite.open_database(database))(db =>
    1.14 +    using(SQLite.open_database(store.the_database(session_name)))(db =>
    1.15      {
    1.16        db.transaction {
    1.17          val export_names = read_theory_names(db, session_name)
     2.1 --- a/src/Pure/Thy/sessions.scala	Thu May 17 15:38:36 2018 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Thu May 17 16:42:13 2018 +0200
     2.3 @@ -1025,6 +1025,9 @@
     2.4      def find_database(name: String): Option[Path] =
     2.5        input_dirs.map(_ + database(name)).find(_.is_file)
     2.6  
     2.7 +    def the_database(name: String): Path =
     2.8 +      find_database(name) getOrElse error("Missing database for session " + quote(name))
     2.9 +
    2.10      def heap(name: String): Path =
    2.11        input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
    2.12          error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +