tuned signature;
authorwenzelm
Fri May 18 17:21:12 2018 +0200 (14 months ago)
changeset 6821065f79c0ddb0d
parent 68209 aeffd8f1f079
child 68211 1e7defef8c8a
tuned signature;
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/export.scala	Fri May 18 17:09:55 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Fri May 18 17:21:12 2018 +0200
     1.3 @@ -254,7 +254,7 @@
     1.4  
     1.5      val store = Sessions.store(options, system_mode)
     1.6  
     1.7 -    using(SQLite.open_database(store.the_database(session_name)))(db =>
     1.8 +    using(store.open_database(session_name))(db =>
     1.9      {
    1.10        db.transaction {
    1.11          val export_names = read_theory_names(db, session_name)
     2.1 --- a/src/Pure/Thy/export_theory.scala	Fri May 18 17:09:55 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Fri May 18 17:21:12 2018 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4      consts: Boolean = true): Session =
     2.5    {
     2.6      val thys =
     2.7 -      using(SQLite.open_database(store.the_database(session_name)))(db =>
     2.8 +      using(store.open_database(session_name))(db =>
     2.9        {
    2.10          db.transaction {
    2.11            Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
     3.1 --- a/src/Pure/Thy/sessions.scala	Fri May 18 17:09:55 2018 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 18 17:21:12 2018 +0200
     3.3 @@ -1026,8 +1026,9 @@
     3.4      def find_database(name: String): Option[Path] =
     3.5        input_dirs.map(_ + database(name)).find(_.is_file)
     3.6  
     3.7 -    def the_database(name: String): Path =
     3.8 -      find_database(name) getOrElse error("Missing database for session " + quote(name))
     3.9 +    def open_database(name: String): SQL.Database =
    3.10 +      SQLite.open_database(
    3.11 +        find_database(name) getOrElse error("Missing database for session " + quote(name)))
    3.12  
    3.13      def heap(name: String): Path =
    3.14        input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse