clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
--- a/src/Pure/Admin/build_log.scala Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/Admin/build_log.scala Tue Jul 18 12:19:12 2023 +0200
@@ -631,6 +631,9 @@
/* SQL data model */
object Data extends SQL.Data("isabelle_build_log") {
+ override def tables: SQL.Tables = ???
+
+
/* main content */
val log_name = SQL.Column.string("log_name").make_primary_key
--- a/src/Pure/General/sql.scala Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/General/sql.scala Tue Jul 18 12:19:12 2023 +0200
@@ -230,15 +230,12 @@
object Tables {
def list(list: List[Table]): Tables = new Tables(list)
- val empty: Tables = list(Nil)
def apply(args: Table*): Tables = list(args.toList)
}
final class Tables private(val list: List[Table]) extends Iterable[Table] {
override def toString: String = list.mkString("SQL.Tables(", ", ", ")")
- def ::: (other: Tables): Tables = new Tables(other.list ::: list)
-
def iterator: Iterator[Table] = list.iterator
// requires transaction
@@ -251,7 +248,7 @@
}
abstract class Data(table_prefix: String = "") {
- def tables: Tables = Tables.empty
+ def tables: Tables
def transaction_lock[A](
db: Database,
@@ -384,13 +381,13 @@
def is_sqlite: Boolean = isInstanceOf[SQLite.Database]
def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
- def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
- if (tables.list.nonEmpty) {
+ def vacuum(tables: List[SQL.Table] = Nil): Unit =
+ if (tables.nonEmpty) {
postgresql_major_version match {
case Some(m) if m <= 10 =>
for (table <- tables) execute_statement("VACUUM " + table.ident)
case Some(_) =>
- execute_statement("VACUUM" + commas(tables.list.map(_.ident)))
+ execute_statement("VACUUM" + commas(tables.map(_.ident)))
case None => execute_statement("VACUUM")
}
}
--- a/src/Pure/System/progress.scala Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/System/progress.scala Tue Jul 18 12:19:12 2023 +0200
@@ -291,7 +291,7 @@
stmt.long(10) = 0L
})
}
- if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables)
+ if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables.list)
}
def exit(close: Boolean = false): Unit = synchronized {
--- a/src/Pure/Tools/build_process.scala Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Tue Jul 18 12:19:12 2023 +0200
@@ -861,15 +861,18 @@
private val _build_database: Option[SQL.Database] =
try {
for (db <- store.maybe_open_build_database(server = server)) yield {
- val store_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
+ val store_tables = db.is_postgresql
Build_Process.Data.transaction_lock(db,
create = true,
label = "Build_Process.build_database"
) {
Build_Process.Data.clean_build(db)
- store_tables.lock(db, create = true)
+ if (store_tables) Store.Data.tables.lock(db, create = true)
}
- if (build_context.master) db.vacuum(Build_Process.Data.tables ::: store_tables)
+ if (build_context.master) {
+ db.vacuum(Build_Process.Data.tables.list :::
+ (if (store_tables) Store.Data.tables.list else Nil))
+ }
db
}
}