# HG changeset patch
# User wenzelm
# Date 1693741136 -7200
# Node ID 163c392675dcf3e9cad74f02d5d0aee2e87ff4a3
# Parent  26a02b042fe0d8ae32a53ad853264ddd91ab4d6f
support "isabelle build_process -r -f";

diff -r 26a02b042fe0 -r 163c392675dc src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 03 13:23:51 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 03 13:38:56 2023 +0200
@@ -503,6 +503,8 @@
   def build_process(
     options: Options,
     list_builds: Boolean = false,
+    remove_builds: Boolean = false,
+    force: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     val build_engine = Engine(engine_name(options))
@@ -510,9 +512,29 @@
 
     using(store.open_server()) { server =>
       using_optional(store.maybe_open_build_database(server = server)) { build_database =>
-        val builds = read_builds(build_database)
+        def print(builds: List[Build_Process.Build]): Unit =
+          if (list_builds) progress.echo(print_builds(build_database, builds))
 
-        if (list_builds) progress.echo(print_builds(build_database, builds))
+        build_database match {
+          case None => print(Nil)
+          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(build => if (build.active) None else Some(build.build_uuid))
+
+              print(builds)
+              if (remove.nonEmpty) {
+                if (remove_builds) {
+                  progress.echo("Removing " + commas(remove) + " ...")
+                  Build_Process.private_data.remove_builds(db, remove)
+                  print(Build_Process.private_data.read_builds(db))
+                }
+              }
+            }
+        }
       }
     }
   }
@@ -520,29 +542,37 @@
   val isabelle_tool2 = Isabelle_Tool("build_process", "manage session build process",
     Scala_Project.here,
     { args =>
+      var force = false
       var list_builds = false
       var options =
         Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
           List(
             Options.Spec.make("build_database_server"),
             Options.Spec.make("build_database")))
+      var remove_builds = false
 
       val getopts = Getopts("""
 Usage: isabelle build_process [OPTIONS]
 
   Options are:
+    -f           extra force for option -r
     -l           list build processes
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -r           remove data from build processes: inactive processes (default)
+                 or all processes (option -f)
 """,
+        "f" -> (_ => force = true),
         "l" -> (_ => list_builds = true),
-        "o:" -> (arg => options = options + arg))
+        "o:" -> (arg => options = options + arg),
+        "r" -> (_ => remove_builds = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress()
 
-      build_process(options, list_builds = list_builds, progress = progress)
+      build_process(options, list_builds = list_builds, remove_builds = remove_builds,
+        force = force, progress = progress)
     })