# HG changeset patch
# User wenzelm
# Date 1678114588 -3600
# Node ID 97b5547f2b17b0af00e7c247fb17d863b7165104
# Parent  2da5562114c5d0920d3d0009a4436dacd4735e29
tuned whitespace and braces;

diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -906,23 +906,18 @@
       db.using_statement(table.select(List(column), distinct = true))(stmt =>
         stmt.execute_query().iterator(_.string(column)).toSet)
 
-    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit = {
-      val table = Data.meta_info_table
-      db.execute_statement(db.insert_permissive(table), body =
+    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
+      db.execute_statement(db.insert_permissive(Data.meta_info_table), body =
         { stmt =>
           stmt.string(1) = log_name
-          for ((c, i) <- table.columns.tail.zipWithIndex) {
-            if (c.T == SQL.Type.Date)
-              stmt.date(i + 2) = meta_info.get_date(c)
-            else
-              stmt.string(i + 2) = meta_info.get(c)
+          for ((c, i) <- Data.meta_info_table.columns.tail.zipWithIndex) {
+            if (c.T == SQL.Type.Date) stmt.date(i + 2) = meta_info.get_date(c)
+            else stmt.string(i + 2) = meta_info.get(c)
           }
         })
-    }
 
-    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
-      val table = Data.sessions_table
-      db.execute_statement(db.insert_permissive(table), body =
+    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
+      db.execute_statement(db.insert_permissive(Data.sessions_table), body =
         { stmt =>
           val sessions =
             if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
@@ -947,11 +942,9 @@
             stmt.string(17) = session.sources
           }
         })
-    }
 
-    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
-      val table = Data.theories_table
-      db.execute_statement(db.insert_permissive(table), body =
+    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
+      db.execute_statement(db.insert_permissive(Data.theories_table), body =
         { stmt =>
           val sessions =
             if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
@@ -969,11 +962,9 @@
             stmt.long(6) = timing.gc.ms
           }
         })
-    }
 
-    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
-      val table = Data.ml_statistics_table
-      db.execute_statement(db.insert_permissive(table), body =
+    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
+      db.execute_statement(db.insert_permissive(Data.ml_statistics_table), body =
         { stmt =>
           val ml_stats: List[(String, Option[Bytes])] =
             Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
@@ -986,7 +977,6 @@
             stmt.bytes(3) = ml_statistics
           }
         })
-    }
 
     def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit = {
       abstract class Table_Status(table: SQL.Table) {
diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -549,8 +549,7 @@
       execute_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))
 
     def notify(name: String, payload: String = ""): Unit =
-      execute_statement(
-        "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))
+      execute_statement("NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))
 
     def get_notifications(): List[PGNotification] =
       the_postgresql_connection.getNotifications() match {
diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/System/host.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -114,8 +114,7 @@
 
     def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
       if (read_numa_next(db, hostname) != numa_next) {
-        db.execute_statement(
-          Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
+        db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
         db.execute_statement(Node_Info.table.insert(), body =
           { stmt =>
             stmt.string(1) = hostname
diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -99,7 +99,7 @@
     }
   }
 
-  def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {
+  def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
     db.execute_statement(Data.table.insert(), body =
       { stmt =>
         stmt.string(1) = session_name
@@ -108,7 +108,6 @@
         stmt.bytes(4) = doc.log_xz
         stmt.bytes(5) = doc.pdf
       })
-  }
 
 
   /* background context */
diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -1565,8 +1565,7 @@
 
         db.create_table(Document_Build.Data.table)
         db.execute_statement(
-          Document_Build.Data.table.delete(
-            sql = Document_Build.Data.session_name.where_equal(name)))
+          Document_Build.Data.table.delete(sql = Document_Build.Data.session_name.where_equal(name)))
       }
     }
 
@@ -1657,7 +1656,7 @@
 
     /* session sources */
 
-    def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit = {
+    def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit =
       for (source_file <- sources) {
         db.execute_statement(Sources.table.insert(), body =
           { stmt =>
@@ -1668,7 +1667,6 @@
             stmt.bytes(5) = source_file.body
           })
       }
-    }
 
     def read_sources(
       db: SQL.Database,
diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -442,7 +442,7 @@
           sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
       )(stmt => stmt.execute_query().iterator(_.long(Workers.serial)).nextOption.getOrElse(0L))
 
-    def set_serial(db: SQL.Database, worker_uuid: String, build_uuid: String, serial: Long): Unit = {
+    def set_serial(db: SQL.Database, worker_uuid: String, build_uuid: String, serial: Long): Unit =
       if (get_serial(db, worker_uuid = worker_uuid) != serial) {
         db.execute_statement(
           Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid))))
@@ -454,7 +454,6 @@
             stmt.long(4) = serial
           })
       }
-    }
 
 
     /* pending jobs */