# HG changeset patch
# User wenzelm
# Date 1710068626 -3600
# Node ID f7dfe92e67857bd759d3ca1283b96df3ddedd590
# Parent  3d83a2554a712415a0f0186b4fb4c921d5cba152
more thorough "isabelle build_process -C -r -f";

diff -r 3d83a2554a71 -r f7dfe92e6785 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sun Mar 10 12:03:13 2024 +0100
+++ b/src/Pure/Build/build.scala	Sun Mar 10 12:03:46 2024 +0100
@@ -517,17 +517,26 @@
 
         build_database match {
           case None => print(Nil)
+          case Some(db) if remove_builds && force =>
+            db.transaction {
+              val tables0 =
+                ML_Heap.private_data.tables.list :::
+                Store.private_data.tables.list :::
+                Progress.private_data.tables.list :::
+                Build_Process.private_data.tables.list
+              val tables = tables0.filter(t => db.exists_table(t.name)).sortBy(_.name)
+              if (tables.nonEmpty) {
+                progress.echo("Removing tables " + commas_quote(tables.map(_.name)) + " ...")
+                db.execute_statement(SQL.MULTI(tables.map(db.destroy)))
+              }
+            }
           case Some(db) =>
             Build_Process.private_data.transaction_lock(db, create = true, label = "build_process") {
               val builds = Build_Process.private_data.read_builds(db)
-              val remove =
-                if (!remove_builds) Nil
-                else if (force) builds.map(_.build_uuid)
-                else builds.flatMap(_.active_build_uuid)
-
               print(builds)
-              if (remove.nonEmpty) {
-                if (remove_builds) {
+              if (remove_builds) {
+                val remove = builds.flatMap(_.active_build_uuid)
+                if (remove.nonEmpty) {
                   progress.echo("Removing " + commas(remove) + " ...")
                   Build_Process.private_data.remove_builds(db, remove)
                   print(Build_Process.private_data.read_builds(db))