# 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()) }