--- a/src/Pure/Tools/build_process.scala Wed Mar 08 15:22:57 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 08 15:25:55 2023 +0100
@@ -465,6 +465,29 @@
val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
}
+ def read_workers(
+ db: SQL.Database,
+ build_uuid: String = "",
+ worker_uuid: String = ""
+ ): State.Workers = {
+ db.execute_query_statement(
+ Workers.table.select(sql =
+ SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
+ List.from[Worker],
+ { res =>
+ Worker(
+ worker_uuid = res.string(Workers.worker_uuid),
+ build_uuid = res.string(Workers.build_uuid),
+ hostname = res.string(Workers.hostname),
+ java_pid = res.long(Workers.java_pid),
+ java_start = res.get_date(Workers.java_start),
+ start = res.date(Workers.start),
+ stamp = res.date(Workers.stamp),
+ stop = res.get_date(Workers.stop),
+ serial = res.long(Workers.serial))
+ })
+ }
+
def serial_max(db: SQL.Database): Long =
db.execute_query_statementO[Long](
Workers.table.select(List(Workers.serial_max)),
@@ -529,29 +552,6 @@
})
}
- def read_workers(
- db: SQL.Database,
- build_uuid: String = "",
- worker_uuid: String = ""
- ): State.Workers = {
- db.execute_query_statement(
- Workers.table.select(sql =
- SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
- List.from[Worker],
- { res =>
- Worker(
- worker_uuid = res.string(Workers.worker_uuid),
- build_uuid = res.string(Workers.build_uuid),
- hostname = res.string(Workers.hostname),
- java_pid = res.long(Workers.java_pid),
- java_start = res.get_date(Workers.java_start),
- start = res.date(Workers.start),
- stamp = res.date(Workers.stamp),
- stop = res.get_date(Workers.stop),
- serial = res.long(Workers.serial))
- })
- }
-
/* pending jobs */