--- a/src/Pure/Thy/sessions.scala Mon Mar 13 15:53:31 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Mar 13 16:53:08 2023 +0100
@@ -1470,7 +1470,7 @@
cat_lines(input_dirs.map(dir => " " + File.standard_path(dir))))
- /* database */
+ /* databases for build process and session content */
def find_database(name: String): Option[Path] =
input_dirs.map(_ + database(name)).find(_.is_file)
@@ -1492,6 +1492,18 @@
port = options.int("build_database_ssh_port"))),
ssh_close = true)
+ val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+
+ def open_build_database(): Option[SQL.Database] =
+ if (!options.bool("build_database_test")) None
+ else if (database_server) Some(open_database_server())
+ else {
+ val db = SQLite.open_database(build_database)
+ try { Isabelle_System.chmod("600", build_database) }
+ catch { case exn: Throwable => db.close(); throw exn }
+ Some(db)
+ }
+
def try_open_database(
name: String,
output: Boolean = false,
--- a/src/Pure/Tools/build_process.scala Mon Mar 13 15:53:31 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 13 16:53:08 2023 +0100
@@ -120,18 +120,8 @@
case None => Nil
}
- def open_database(): Option[SQL.Database] =
- if (!build_options.bool("build_database_test")) None
- else if (store.database_server) Some(store.open_database_server())
- else {
- val db = SQLite.open_database(Build_Process.Data.database)
- try { Isabelle_System.chmod("600", Build_Process.Data.database) }
- catch { case exn: Throwable => db.close(); throw exn }
- Some(db)
- }
-
def prepare_database(): Unit = {
- using_option(open_database()) { db =>
+ using_option(store.open_build_database()) { db =>
db.transaction {
Data.all_tables.create_lock(db)
Data.clean_build(db)
@@ -267,8 +257,6 @@
/** SQL data model **/
object Data {
- val database = Path.explode("$ISABELLE_HOME_USER/build.db")
-
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
@@ -782,7 +770,7 @@
private var _state: Build_Process.State = init_state(Build_Process.State())
- private val _database: Option[SQL.Database] = build_context.open_database()
+ private val _database: Option[SQL.Database] = store.open_build_database()
def close(): Unit = synchronized { _database.foreach(_.close()) }