diff -r 721c118f7001 -r 2df0f3604a67 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Jun 21 11:42:11 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Wed Jun 21 14:27:51 2023 +0200 @@ -124,11 +124,11 @@ def prepare_database(): Unit = { using_option(store.maybe_open_build_database(Data.database)) { db => val shared_db = db.is_postgresql - db.transaction_lock(Data.all_tables, create = true) { + Data.transaction_lock(db, create = true) { Data.clean_build(db) - if (shared_db) Store.Data.all_tables.lock(db, create = true) + if (shared_db) Store.Data.tables.lock(db, create = true) } - db.vacuum(Data.all_tables ::: (if (shared_db) Store.Data.all_tables else SQL.Tables.empty)) + Data.vacuum(db, more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty) } } @@ -267,12 +267,9 @@ /** SQL data model **/ - object Data { + object Data extends SQL.Data("isabelle_build") { val database: Path = Path.explode("$ISABELLE_HOME_USER/build.db") - def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = - SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body) - def pull_data[A <: Library.Named]( data_domain: Set[String], data_iterator: Set[String] => Iterator[A], @@ -727,7 +724,7 @@ /* collective operations */ - val all_tables: SQL.Tables = + override val tables = SQL.Tables( Base.table, Workers.table, @@ -737,7 +734,7 @@ Results.table) val build_uuid_tables = - all_tables.filter(table => + tables.filter(table => table.columns.exists(column => column.name == Generic.build_uuid.name)) def pull_database( @@ -845,7 +842,7 @@ _database match { case None => body case Some(db) => - db.transaction_lock(Build_Process.Data.all_tables) { + Build_Process.Data.transaction_lock(db) { progress.asInstanceOf[Database_Progress].sync() _state = Build_Process.Data.pull_database(db, worker_uuid, hostname, _state) val res = body