# HG changeset patch # User wenzelm # Date 1678722788 -3600 # Node ID 979baa91da0f31c2af8ef67943fe930abee96f10 # Parent a538dab533ef4befa6976157527b7af77ad57b8e clarified modules; diff -r a538dab533ef -r 979baa91da0f src/Pure/Thy/sessions.scala --- 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, diff -r a538dab533ef -r 979baa91da0f src/Pure/Tools/build_process.scala --- 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()) }