# HG changeset patch # User wenzelm # Date 1678285555 -3600 # Node ID 80021d645a01699ef141b763bacb9a28326cf0da # Parent 89c42ec77a844cde3d0c570c9f0a93ebfe61aa39 tuned structure; diff -r 89c42ec77a84 -r 80021d645a01 src/Pure/Tools/build_process.scala --- 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 */