--- 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