src/Pure/Tools/build_process.scala
changeset 77534 fc57886e37dd
parent 77533 8f464df3520a
child 77536 7c7f1473e51a
--- 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