--- a/src/Pure/Admin/build_log.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Mar 06 15:38:50 2023 +0100
@@ -908,84 +908,84 @@
def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit = {
val table = Data.meta_info_table
- db.using_statement(db.insert_permissive(table)) { 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)
- }
- stmt.execute()
- }
+ db.execute_statement(db.insert_permissive(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)
+ }
+ })
}
def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
val table = Data.sessions_table
- db.using_statement(db.insert_permissive(table)) { stmt =>
- val sessions =
- if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
- else build_info.sessions
- for ((session_name, session) <- sessions) {
- stmt.string(1) = log_name
- stmt.string(2) = session_name
- stmt.string(3) = proper_string(session.chapter)
- stmt.string(4) = session.proper_groups
- stmt.int(5) = session.threads
- stmt.long(6) = session.timing.elapsed.proper_ms
- stmt.long(7) = session.timing.cpu.proper_ms
- stmt.long(8) = session.timing.gc.proper_ms
- stmt.double(9) = session.timing.factor
- stmt.long(10) = session.ml_timing.elapsed.proper_ms
- stmt.long(11) = session.ml_timing.cpu.proper_ms
- stmt.long(12) = session.ml_timing.gc.proper_ms
- stmt.double(13) = session.ml_timing.factor
- stmt.long(14) = session.heap_size.map(_.bytes)
- stmt.string(15) = session.status.map(_.toString)
- stmt.bytes(16) = compress_errors(session.errors, cache = cache.compress)
- stmt.string(17) = session.sources
- stmt.execute()
- }
- }
+ db.execute_statement(db.insert_permissive(table), body =
+ { stmt =>
+ val sessions =
+ if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
+ else build_info.sessions
+ for ((session_name, session) <- sessions) {
+ stmt.string(1) = log_name
+ stmt.string(2) = session_name
+ stmt.string(3) = proper_string(session.chapter)
+ stmt.string(4) = session.proper_groups
+ stmt.int(5) = session.threads
+ stmt.long(6) = session.timing.elapsed.proper_ms
+ stmt.long(7) = session.timing.cpu.proper_ms
+ stmt.long(8) = session.timing.gc.proper_ms
+ stmt.double(9) = session.timing.factor
+ stmt.long(10) = session.ml_timing.elapsed.proper_ms
+ stmt.long(11) = session.ml_timing.cpu.proper_ms
+ stmt.long(12) = session.ml_timing.gc.proper_ms
+ stmt.double(13) = session.ml_timing.factor
+ stmt.long(14) = session.heap_size.map(_.bytes)
+ stmt.string(15) = session.status.map(_.toString)
+ stmt.bytes(16) = compress_errors(session.errors, cache = cache.compress)
+ 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.using_statement(db.insert_permissive(table)) { stmt =>
- val sessions =
- if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
- Build_Info.sessions_dummy
- else build_info.sessions
- for {
- (session_name, session) <- sessions
- (theory_name, timing) <- session.theory_timings
- } {
- stmt.string(1) = log_name
- stmt.string(2) = session_name
- stmt.string(3) = theory_name
- stmt.long(4) = timing.elapsed.ms
- stmt.long(5) = timing.cpu.ms
- stmt.long(6) = timing.gc.ms
- stmt.execute()
- }
- }
+ db.execute_statement(db.insert_permissive(table), body =
+ { stmt =>
+ val sessions =
+ if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
+ Build_Info.sessions_dummy
+ else build_info.sessions
+ for {
+ (session_name, session) <- sessions
+ (theory_name, timing) <- session.theory_timings
+ } {
+ stmt.string(1) = log_name
+ stmt.string(2) = session_name
+ stmt.string(3) = theory_name
+ stmt.long(4) = timing.elapsed.ms
+ stmt.long(5) = timing.cpu.ms
+ 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.using_statement(db.insert_permissive(table)) { stmt =>
- val ml_stats: List[(String, Option[Bytes])] =
- Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
- { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.compress).proper) },
- build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
- val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
- for ((session_name, ml_statistics) <- entries) {
- stmt.string(1) = log_name
- stmt.string(2) = session_name
- stmt.bytes(3) = ml_statistics
- stmt.execute()
- }
- }
+ db.execute_statement(db.insert_permissive(table), body =
+ { stmt =>
+ val ml_stats: List[(String, Option[Bytes])] =
+ Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
+ { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.compress).proper) },
+ build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
+ val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
+ for ((session_name, ml_statistics) <- entries) {
+ stmt.string(1) = log_name
+ stmt.string(2) = session_name
+ stmt.bytes(3) = ml_statistics
+ }
+ })
}
def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit = {
--- a/src/Pure/General/sql.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/General/sql.scala Mon Mar 06 15:38:50 2023 +0100
@@ -377,7 +377,8 @@
def using_statement[A](sql: Source)(f: Statement => A): A =
using(statement(sql))(f)
- def execute_statement(sql: Source): Unit = using_statement(sql)(_.execute())
+ def execute_statement(sql: Source, body: Statement => Unit = _ => ()): Unit =
+ using_statement(sql) { stmt => body(stmt); stmt.execute() }
def update_date(stmt: Statement, i: Int, date: Date): Unit
def date(res: Result, column: Column): Date
@@ -543,14 +544,14 @@
// see https://www.postgresql.org/docs/current/sql-notify.html
def listen(name: String): Unit =
- using_statement("LISTEN " + SQL.ident(name))(_.execute())
+ execute_statement("LISTEN " + SQL.ident(name))
def unlisten(name: String = "*"): Unit =
- using_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))(_.execute())
+ execute_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))
def notify(name: String, payload: String = ""): Unit =
- using_statement(
- "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))(_.execute())
+ 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:12:37 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 15:38:50 2023 +0100
@@ -114,14 +114,13 @@
def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
if (read_numa_next(db, hostname) != numa_next) {
- db.using_statement(
- Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))
- )(_.execute())
- db.using_statement(Node_Info.table.insert()) { stmt =>
- stmt.string(1) = hostname
- stmt.int(2) = numa_next
- stmt.execute()
- }
+ 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
+ stmt.int(2) = numa_next
+ })
true
}
else false
--- a/src/Pure/Thy/document_build.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Mon Mar 06 15:38:50 2023 +0100
@@ -100,14 +100,14 @@
}
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {
- db.using_statement(Data.table.insert()){ stmt =>
- stmt.string(1) = session_name
- stmt.string(2) = doc.name
- stmt.string(3) = doc.sources.toString
- stmt.bytes(4) = doc.log_xz
- stmt.bytes(5) = doc.pdf
- stmt.execute()
- }
+ db.execute_statement(Data.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = session_name
+ stmt.string(2) = doc.name
+ stmt.string(3) = doc.sources.toString
+ stmt.bytes(4) = doc.log_xz
+ stmt.bytes(5) = doc.pdf
+ })
}
--- a/src/Pure/Thy/export.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Thy/export.scala Mon Mar 06 15:38:50 2023 +0100
@@ -165,15 +165,15 @@
def write(db: SQL.Database): Unit = {
val (compressed, bs) = body.join
- db.using_statement(Data.table.insert()) { stmt =>
- stmt.string(1) = session_name
- stmt.string(2) = theory_name
- stmt.string(3) = name
- stmt.bool(4) = executable
- stmt.bool(5) = compressed
- stmt.bytes(6) = bs
- stmt.execute()
- }
+ db.execute_statement(Data.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = session_name
+ stmt.string(2) = theory_name
+ stmt.string(3) = name
+ stmt.bool(4) = executable
+ stmt.bool(5) = compressed
+ stmt.bytes(6) = bs
+ })
}
}
--- a/src/Pure/Thy/sessions.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Mar 06 15:38:50 2023 +0100
@@ -1592,21 +1592,21 @@
): Unit = {
db.transaction {
write_sources(db, session_name, sources)
- db.using_statement(Session_Info.table.insert()) { stmt =>
- stmt.string(1) = session_name
- stmt.bytes(2) = Properties.encode(build_log.session_timing)
- stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
- stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
- stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
- stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
- stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
- stmt.string(8) = build.sources.toString
- stmt.string(9) = build.input_heaps.toString
- stmt.string(10) = build.output_heap.toString
- stmt.int(11) = build.return_code
- stmt.string(12) = build.uuid
- stmt.execute()
- }
+ db.execute_statement(Session_Info.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = session_name
+ stmt.bytes(2) = Properties.encode(build_log.session_timing)
+ stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
+ stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
+ stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
+ stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
+ stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
+ stmt.string(8) = build.sources.toString
+ stmt.string(9) = build.input_heaps.toString
+ stmt.string(10) = build.output_heap.toString
+ stmt.int(11) = build.return_code
+ stmt.string(12) = build.uuid
+ })
}
}
@@ -1659,14 +1659,14 @@
def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit = {
for (source_file <- sources) {
- db.using_statement(Sources.table.insert()) { stmt =>
- stmt.string(1) = session_name
- stmt.string(2) = source_file.name
- stmt.string(3) = source_file.digest.toString
- stmt.bool(4) = source_file.compressed
- stmt.bytes(5) = source_file.body
- stmt.execute()
- }
+ db.execute_statement(Sources.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = session_name
+ stmt.string(2) = source_file.name
+ stmt.string(3) = source_file.digest.toString
+ stmt.bool(4) = source_file.compressed
+ stmt.bytes(5) = source_file.body
+ })
}
}
--- a/src/Pure/Tools/build_process.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 06 15:38:50 2023 +0100
@@ -287,23 +287,20 @@
ml_platform: String,
options: String
): Unit = {
- db.using_statement(Base.table.insert()) { stmt =>
- stmt.string(1) = build_uuid
- stmt.string(2) = ml_platform
- stmt.string(3) = options
- stmt.date(4) = db.now()
- stmt.date(5) = None
- stmt.execute()
- }
+ db.execute_statement(Base.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = build_uuid
+ stmt.string(2) = ml_platform
+ stmt.string(3) = options
+ stmt.date(4) = db.now()
+ stmt.date(5) = None
+ })
}
def end_build(db: SQL.Database, build_uuid: String): Unit =
- db.using_statement(
- Base.table.update(List(Base.end), sql = SQL.where(Generic.sql(build_uuid = build_uuid)))
- ) { stmt =>
- stmt.date(1) = db.now()
- stmt.execute()
- }
+ db.execute_statement(
+ Base.table.update(List(Base.end), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+ body = { stmt => stmt.date(1) = db.now() })
def clean_build(db: SQL.Database): Unit = {
val old =
@@ -362,17 +359,17 @@
val insert = sessions.iterator.filterNot(p => old_sessions.contains(p._1)).toList
for ((name, session) <- insert) {
- db.using_statement(Sessions.table.insert()) { stmt =>
- stmt.string(1) = name
- stmt.string(2) = cat_lines(session.deps)
- stmt.string(3) = cat_lines(session.ancestors)
- stmt.string(4) = session.sources_shasum.toString
- stmt.long(5) = session.timeout.ms
- stmt.long(6) = session.old_time.ms
- stmt.bytes(7) = session.old_command_timings_blob
- stmt.string(8) = session.build_uuid
- stmt.execute()
- }
+ db.execute_statement(Sessions.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = name
+ stmt.string(2) = cat_lines(session.deps)
+ stmt.string(3) = cat_lines(session.ancestors)
+ stmt.string(4) = session.sources_shasum.toString
+ stmt.long(5) = session.timeout.ms
+ stmt.long(6) = session.old_time.ms
+ stmt.bytes(7) = session.old_command_timings_blob
+ stmt.string(8) = session.build_uuid
+ })
}
insert.nonEmpty
@@ -415,14 +412,14 @@
message: isabelle.Progress.Message,
build_uuid: String
): Unit = {
- db.using_statement(Progress.table.insert()) { stmt =>
- stmt.long(1) = message_serial
- stmt.int(2) = message.kind.id
- stmt.string(3) = message.text
- stmt.bool(4) = message.verbose
- stmt.string(5) = build_uuid
- stmt.execute()
- }
+ db.execute_statement(Progress.table.insert(), body =
+ { stmt =>
+ stmt.long(1) = message_serial
+ stmt.int(2) = message.kind.id
+ stmt.string(3) = message.text
+ stmt.bool(4) = message.verbose
+ stmt.string(5) = build_uuid
+ })
}
@@ -449,13 +446,13 @@
if (get_serial(db, worker_uuid = worker_uuid) != serial) {
db.execute_statement(
Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid))))
- db.using_statement(Workers.table.insert()) { stmt =>
- stmt.string(1) = worker_uuid
- stmt.string(2) = build_uuid
- stmt.date(3) = db.now()
- stmt.long(4) = serial
- stmt.execute()
- }
+ db.execute_statement(Workers.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = worker_uuid
+ stmt.string(2) = build_uuid
+ stmt.date(3) = db.now()
+ stmt.long(4) = serial
+ })
}
}
@@ -491,12 +488,12 @@
}
for (entry <- insert) {
- db.using_statement(Pending.table.insert()) { stmt =>
- stmt.string(1) = entry.name
- stmt.string(2) = cat_lines(entry.deps)
- stmt.string(3) = JSON.Format(entry.info)
- stmt.execute()
- }
+ db.execute_statement(Pending.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = entry.name
+ stmt.string(2) = cat_lines(entry.deps)
+ stmt.string(3) = JSON.Format(entry.info)
+ })
}
delete.nonEmpty || insert.nonEmpty
@@ -536,12 +533,12 @@
}
for (job <- insert) {
- db.using_statement(Running.table.insert()) { stmt =>
- stmt.string(1) = job.job_name
- stmt.string(2) = job.node_info.hostname
- stmt.int(3) = job.node_info.numa_node
- stmt.execute()
- }
+ db.execute_statement(Running.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = job.job_name
+ stmt.string(2) = job.node_info.hostname
+ stmt.int(3) = job.node_info.numa_node
+ })
}
delete.nonEmpty || insert.nonEmpty
@@ -603,18 +600,18 @@
for ((name, result) <- insert) {
val node_info = result.node_info
val process_result = result.process_result
- db.using_statement(Results.table.insert()) { stmt =>
- stmt.string(1) = name
- stmt.string(2) = node_info.hostname
- stmt.int(3) = node_info.numa_node
- stmt.int(4) = process_result.rc
- stmt.string(5) = cat_lines(process_result.out_lines)
- stmt.string(6) = cat_lines(process_result.err_lines)
- stmt.long(7) = process_result.timing.elapsed.ms
- stmt.long(8) = process_result.timing.cpu.ms
- stmt.long(9) = process_result.timing.gc.ms
- stmt.execute()
- }
+ db.execute_statement(Results.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = name
+ stmt.string(2) = node_info.hostname
+ stmt.int(3) = node_info.numa_node
+ stmt.int(4) = process_result.rc
+ stmt.string(5) = cat_lines(process_result.out_lines)
+ stmt.string(6) = cat_lines(process_result.err_lines)
+ stmt.long(7) = process_result.timing.elapsed.ms
+ stmt.long(8) = process_result.timing.cpu.ms
+ stmt.long(9) = process_result.timing.gc.ms
+ })
}
insert.nonEmpty
--- a/src/Pure/Tools/server.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/Tools/server.scala Mon Mar 06 15:38:50 2023 +0100
@@ -410,12 +410,12 @@
val server_info = Info(name, server.port, server.password)
db.execute_statement(Data.table.delete(sql = Data.name.where_equal(name)))
- db.using_statement(Data.table.insert()) { stmt =>
- stmt.string(1) = server_info.name
- stmt.int(2) = server_info.port
- stmt.string(3) = server_info.password
- stmt.execute()
- }
+ db.execute_statement(Data.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = server_info.name
+ stmt.int(2) = server_info.port
+ stmt.string(3) = server_info.password
+ })
server.start()
(server_info, Some(server))