# HG changeset patch
# User wenzelm
# Date 1700939924 -3600
# Node ID ad7f485195df77ebadd2af9981376b528e55efc7
# Parent  6977fb0153fb9a61b0f0cc1d7dbcdda2d4ee6d55
clarified modules;
clarified transactions;

diff -r 6977fb0153fb -r ad7f485195df src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 25 20:09:20 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 25 20:18:44 2023 +0100
@@ -797,6 +797,23 @@
 
     /* access data */
 
+    def read_domain(
+      db: SQL.Database,
+      table: SQL.Table,
+      column: SQL.Column,
+      restriction: Option[Iterable[String]] = None,
+      cache: XML.Cache = XML.Cache.make()
+    ): Set[String] = {
+      db.execute_query_statement(
+        table.select(List(column),
+          sql = restriction match {
+            case None => ""
+            case Some(names) => column.where_member(names)
+          },
+          distinct = true),
+        Set.from[String], res => cache.string(res.string(column)))
+    }
+
     def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
       val table = meta_info_table
       val columns = table.columns.tail
@@ -999,7 +1016,7 @@
         ssh_user = options.string("build_log_ssh_user"))
 
     def init_database(db: SQL.Database, minimal: Boolean = false): Unit =
-      private_data.transaction_lock(db, create = true, label = "build_log_init") {
+      private_data.transaction_lock(db, create = true, label = "Build_Log.init_database") {
         if (!minimal) {
           db.create_view(private_data.pull_date_table())
           db.create_view(private_data.pull_date_table(afp = true))
@@ -1071,24 +1088,6 @@
       }
     }
 
-    def read_domain(
-      db: SQL.Database,
-      table: SQL.Table,
-      column: SQL.Column,
-      restriction: Option[Iterable[String]] = None
-    ): Set[String] = {
-      private_data.transaction_lock(db, label = "Build_Log.read_domain") {
-        db.execute_query_statement(
-          table.select(List(column),
-            sql = restriction match {
-              case None => ""
-              case Some(names) => column.where_member(names)
-            },
-            distinct = true),
-          Set.from[String], res => cache.string(res.string(column)))
-      }
-    }
-
     def write_info(db: SQL.Database, files: List[JFile],
       ml_statistics: Boolean = false,
       progress: Progress = new Progress,
@@ -1107,7 +1106,9 @@
 
       abstract class Table_Status(table: SQL.Table) {
         private val known =
-          Synchronized(read_domain(db, table, private_data.log_name, restriction = files_domain))
+          Synchronized(
+            private_data.read_domain(db, table, private_data.log_name,
+              restriction = files_domain, cache = cache))
 
         def required(file: JFile): Boolean = !(known.value)(Log_File.plain_name(file))
         def required(log_file: Log_File): Boolean = !(known.value)(log_file.name)
@@ -1121,32 +1122,35 @@
         }
       }
 
-      val ml_statistics_status =
-        if (ml_statistics) {
-          List(
-            new Table_Status(private_data.ml_statistics_table) {
-              override def update_db(db: SQL.Database, log_file: Log_File): Unit =
-                private_data.update_ml_statistics(db, cache.compress, log_file.name,
-                  log_file.parse_build_info(ml_statistics = true))
-            })
+      val status =
+        private_data.transaction_lock(db, label = "build_log_database.status") {
+          val status1 =
+            if (ml_statistics) {
+              List(
+                new Table_Status(private_data.ml_statistics_table) {
+                  override def update_db(db: SQL.Database, log_file: Log_File): Unit =
+                    private_data.update_ml_statistics(db, cache.compress, log_file.name,
+                      log_file.parse_build_info(ml_statistics = true))
+                })
+            }
+            else Nil
+          val status2 =
+            List(
+              new Table_Status(private_data.meta_info_table) {
+                override def update_db(db: SQL.Database, log_file: Log_File): Unit =
+                  private_data.update_meta_info(db, log_file.name, log_file.parse_meta_info())
+              },
+              new Table_Status(private_data.sessions_table) {
+                override def update_db(db: SQL.Database, log_file: Log_File): Unit =
+                  private_data.update_sessions(db, cache.compress, log_file.name,
+                    log_file.parse_build_info())
+              },
+              new Table_Status(private_data.theories_table) {
+                override def update_db(db: SQL.Database, log_file: Log_File): Unit =
+                  private_data.update_theories(db, log_file.name, log_file.parse_build_info())
+              })
+          status1 ::: status2
         }
-        else Nil
-      val status =
-        List(
-          new Table_Status(private_data.meta_info_table) {
-            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
-              private_data.update_meta_info(db, log_file.name, log_file.parse_meta_info())
-          },
-          new Table_Status(private_data.sessions_table) {
-            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
-              private_data.update_sessions(db, cache.compress, log_file.name,
-                log_file.parse_build_info())
-          },
-          new Table_Status(private_data.theories_table) {
-            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
-              private_data.update_theories(db, log_file.name, log_file.parse_build_info())
-          }
-        ) ::: ml_statistics_status
 
       val consumer =
         Consumer_Thread.fork[Log_File]("build_log_database")(
@@ -1155,7 +1159,7 @@
             val t0 = progress.start.time
             val t1 = progress.now().time
 
-            private_data.transaction_lock(db, label = "build_log_database") {
+            private_data.transaction_lock(db, label = "build_log_database.consumer") {
               try { status.foreach(_.update(log_file)) }
               catch { case exn: Throwable => add_error(log_file.name, exn) }
             }