# HG changeset patch # User wenzelm # Date 1526656872 -7200 # Node ID 65f79c0ddb0d18c600690e57e23026d247390858 # Parent aeffd8f1f079b687520b265cc8bf67fb5aa33d5c tuned signature; diff -r aeffd8f1f079 -r 65f79c0ddb0d src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Fri May 18 17:09:55 2018 +0200 +++ b/src/Pure/Thy/export.scala Fri May 18 17:21:12 2018 +0200 @@ -254,7 +254,7 @@ val store = Sessions.store(options, system_mode) - using(SQLite.open_database(store.the_database(session_name)))(db => + using(store.open_database(session_name))(db => { db.transaction { val export_names = read_theory_names(db, session_name) diff -r aeffd8f1f079 -r 65f79c0ddb0d src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Fri May 18 17:09:55 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Fri May 18 17:21:12 2018 +0200 @@ -29,7 +29,7 @@ consts: Boolean = true): Session = { val thys = - using(SQLite.open_database(store.the_database(session_name)))(db => + using(store.open_database(session_name))(db => { db.transaction { Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator. diff -r aeffd8f1f079 -r 65f79c0ddb0d src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri May 18 17:09:55 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Fri May 18 17:21:12 2018 +0200 @@ -1026,8 +1026,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 open_database(name: String): SQL.Database = + SQLite.open_database( + 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