clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
authorwenzelm
Tue, 31 Oct 2023 14:26:19 +0100
changeset 78862 cc8391b92747
parent 78861 5c91bd51fc37
child 78863 f627ab8c276c
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
etc/options
src/Pure/Admin/build_log.scala
--- a/etc/options	Sun Oct 29 20:14:46 2023 +0100
+++ b/etc/options	Tue Oct 31 14:26:19 2023 +0100
@@ -417,7 +417,6 @@
 option build_log_ssh_user : string = "" for connection
 option build_log_ssh_port : int = 0 for connection
 option build_log_history : int = 30  -- "length of relevant history (in days)"
-option build_log_transaction_size : int = 1  -- "number of log files for each db update"
 option build_log_database_synchronous_commit : string = "off" (standard "on") for connection
   -- "see https://www.postgresql.org/docs/current/runtime-config-wal.html#GUC-SYNCHRONOUS-COMMIT"
 
--- a/src/Pure/Admin/build_log.scala	Sun Oct 29 20:14:46 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 31 14:26:19 2023 +0100
@@ -1073,23 +1073,16 @@
           }
         ) ::: ml_statistics_status
 
-      val file_groups_iterator =
-        files.filter(file => status.exists(_.required(file))).
-          grouped(options.int("build_log_transaction_size") max 1)
-
-      for (file_group <- file_groups_iterator) {
-        val log_files =
-          Par_List.map[JFile, Exn.Result[Log_File]](
-            file => Exn.result { Log_File(file) }, file_group)
-        private_data.transaction_lock(db, label = "build_log_database") {
-          for (case Exn.Res(log_file) <- log_files) {
-            progress.echo("Log " + quote(log_file.name), verbose = true)
-            try { status.foreach(_.update(log_file)) }
-            catch { case exn: Throwable => add_error(log_file.name, exn) }
-          }
-        }
-        for (case (file, Exn.Exn(exn)) <- file_group.zip(log_files)) {
-          add_error(Log_File.plain_name(file), exn)
+      for (file <- files.iterator if status.exists(_.required(file))) {
+        val log_name = Log_File.plain_name(file)
+        progress.echo("Log " + quote(log_name), verbose = true)
+        Exn.result { Log_File(file) } match {
+          case Exn.Res(log_file) =>
+            private_data.transaction_lock(db, label = "build_log_database") {
+              try { status.foreach(_.update(log_file)) }
+              catch { case exn: Throwable => add_error(log_name, exn) }
+            }
+          case Exn.Exn(exn) => add_error(log_name, exn)
         }
       }