--- a/src/Pure/Tools/build_process.scala Mon Mar 06 10:08:53 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 06 10:16:40 2023 +0100
@@ -572,19 +572,19 @@
/* collective operations */
+ def all_tables: List[SQL.Table] =
+ List(
+ Base.table,
+ Workers.table,
+ Progress.table,
+ Sessions.table,
+ Pending.table,
+ Running.table,
+ Results.table,
+ Host.Data.Node_Info.table)
+
def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
- val tables =
- List(
- Base.table,
- Workers.table,
- Progress.table,
- Sessions.table,
- Pending.table,
- Running.table,
- Results.table,
- Host.Data.Node_Info.table)
-
- for (table <- tables) db.create_table(table)
+ for (table <- all_tables) db.create_table(table)
val old_pending = Data.read_pending(db)
if (old_pending.nonEmpty) {
@@ -592,7 +592,7 @@
commas_quote(old_pending.map(_.name)))
}
- for (table <- tables) db.using_statement(table.delete())(_.execute())
+ for (table <- all_tables) db.using_statement(table.delete())(_.execute())
db.using_statement(Base.table.insert()) { stmt =>
stmt.string(1) = build_context.build_uuid