# HG changeset patch
# User wenzelm
# Date 1698601782 -3600
# Node ID aeb511a520f405b04da02a24f0e091e483552678
# Parent  763dd9bdb101b0722817b2300a870f230f13b6cb
performance tuning: more careful database access;

diff -r 763dd9bdb101 -r aeb511a520f4 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Oct 29 11:57:01 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Oct 29 18:49:42 2023 +0100
@@ -921,10 +921,23 @@
       }
     }
 
-    def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
-      db.execute_query_statement(
-        table.select(List(column), distinct = true),
-        Set.from[String], res => res.string(column))
+    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 update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
       db.execute_statement(db.insert_permissive(private_data.meta_info_table),
@@ -1012,8 +1025,15 @@
         errors1 = errors1.insert(name, Exn.print(exn))
       }
 
+      val files_domain = {
+        val names = files.map(Log_File.plain_name).toSet
+        if (names.size > 100) None else Some(names)
+      }
+
       abstract class Table_Status(table: SQL.Table) {
-        private var known: Set[String] = domain(db, table, private_data.log_name)
+        private var known: Set[String] =
+          read_domain(db, table, private_data.log_name,
+            restriction = files_domain)
 
         def required(file: JFile): Boolean = !known(Log_File.plain_name(file))
         def required(log_file: Log_File): Boolean = !known(log_file.name)
@@ -1026,6 +1046,17 @@
           }
         }
       }
+
+      val ml_statistics_status =
+        if (ml_statistics) Nil
+        else {
+          List(
+            new Table_Status(private_data.ml_statistics_table) {
+              override def update_db(db: SQL.Database, log_file: Log_File): Unit =
+                update_ml_statistics(db, log_file.name,
+                  log_file.parse_build_info(ml_statistics = true))
+            })
+        }
       val status =
         List(
           new Table_Status(private_data.meta_info_table) {
@@ -1039,14 +1070,8 @@
           new Table_Status(private_data.theories_table) {
             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
               update_theories(db, log_file.name, log_file.parse_build_info())
-          },
-          new Table_Status(private_data.ml_statistics_table) {
-            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
-            if (ml_statistics) {
-              update_ml_statistics(db, log_file.name,
-                log_file.parse_build_info(ml_statistics = true))
-            }
-          })
+          }
+        ) ::: ml_statistics_status
 
       val file_groups_iterator =
         files.filter(file => status.exists(_.required(file))).