# HG changeset patch
# User wenzelm
# Date 1708259564 -3600
# Node ID 2a9d8c74eb3c4ffc1cfd1545bef1131588e839a0
# Parent  49475f8bb4cc2ac0b6e2ad2ae2d9d18dd2e67697
clarified signature: emphasize physical db files;

diff -r 49475f8bb4cc -r 2a9d8c74eb3c src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Feb 18 13:01:00 2024 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Feb 18 13:32:44 2024 +0100
@@ -282,7 +282,7 @@
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
         build_info.finished_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.database(session_name)
+          val database = isabelle_output + store.log_db(session_name)
 
           if (database.is_file) {
             using(SQLite.open_database(database)) { db =>
@@ -309,7 +309,7 @@
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
         build_info.finished_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.database(session_name)
+          val database = isabelle_output + store.log_db(session_name)
           val log_gz = isabelle_output + store.log_gz(session_name)
 
           val properties =
@@ -336,7 +336,7 @@
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
         build_info.failed_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.database(session_name)
+          val database = isabelle_output + store.log_db(session_name)
           val errors =
             if (database.is_file) {
               try {
diff -r 49475f8bb4cc -r 2a9d8c74eb3c src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sun Feb 18 13:01:00 2024 +0100
+++ b/src/Pure/Build/store.scala	Sun Feb 18 13:32:44 2024 +0100
@@ -253,13 +253,13 @@
   /* file names */
 
   def heap(name: String): Path = Path.basic(name)
-  def database(name: String): Path = Path.basic("log") + Path.basic(name).db
   def log(name: String): Path = Path.basic("log") + Path.basic(name)
+  def log_db(name: String): Path = log(name).db
   def log_gz(name: String): Path = log(name).gz
 
   def output_heap(name: String): Path = output_dir + heap(name)
-  def output_database(name: String): Path = output_dir + database(name)
   def output_log(name: String): Path = output_dir + log(name)
+  def output_log_db(name: String): Path = output_dir + log_db(name)
   def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
 
@@ -293,8 +293,8 @@
 
   /* databases for build process and session content */
 
-  def find_database(name: String): Option[Path] =
-    input_dirs.map(_ + database(name)).find(_.is_file)
+  def find_log_db(name: String): Option[Path] =
+    input_dirs.map(_ + log_db(name)).find(_.is_file)
 
   def build_database_server: Boolean = options.bool("build_database_server")
   def build_database: Boolean = options.bool("build_database")
@@ -342,11 +342,11 @@
       if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
     if (server_mode) check(open_database_server(server = server))
-    else if (output) Some(SQLite.open_database(output_database(name)))
+    else if (output) Some(SQLite.open_database(output_log_db(name)))
     else {
       (for {
         dir <- input_dirs.view
-        path = dir + database(name) if path.is_file
+        path = dir + log_db(name) if path.is_file
         db <- check(SQLite.open_database(path))
       } yield db).headOption
     }
@@ -380,7 +380,7 @@
       for {
         dir <-
           (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
-        file <- List(heap(name), database(name), log(name), log_gz(name))
+        file <- List(heap(name), log_db(name), log(name), log_gz(name))
         path = dir + file if path.is_file
       } yield path.file.delete
 
diff -r 49475f8bb4cc -r 2a9d8c74eb3c src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sun Feb 18 13:01:00 2024 +0100
+++ b/src/Pure/Tools/sync.scala	Sun Feb 18 13:32:44 2024 +0100
@@ -22,7 +22,7 @@
           store.find_heap(session).map(_.expand).map(path =>
             File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
         val db =
-          store.find_database(session).map(_.expand).map(path =>
+          store.find_log_db(session).map(_.expand).map(path =>
             File.standard_path(path.dir.dir.dir) + "/./" + path.dir.dir.file_name + "/" +
               path.dir.file_name + "/" + path.file_name)
         heap.toList ::: db.toList