--- 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) {
--- 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 {
--- 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
--- 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 */
--- 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,
--- 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 */