# HG changeset patch
# User wenzelm
# Date 1708633735 -3600
# Node ID 32ca3d1283de27ffaf39b1fe16f1742b44749a99
# Parent  90fbcdafb34ec703ee53953a736564a026a66bfa
clarified signature: Build_Process tells how to clean sessions;

diff -r 90fbcdafb34e -r 32ca3d1283de src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Thu Feb 22 21:03:55 2024 +0100
+++ b/src/Pure/Build/build.scala	Thu Feb 22 21:28:55 2024 +0100
@@ -34,6 +34,7 @@
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
+    clean_sessions: List[String] = Nil,
     build_heap: Boolean = false,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
@@ -143,7 +144,10 @@
       server: SSH.Server
     ): Results = {
       Isabelle_Thread.uninterruptible {
-        using(open_build_process(context, progress, server))(_.run())
+        using(open_build_process(context, progress, server)) { build_process =>
+          build_process.prepare()
+          build_process.run()
+        }
       }
     }
   }
@@ -243,19 +247,17 @@
 
         /* build process and results */
 
+        val clean_sessions =
+          if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil
+
         val build_context =
           Context(store, build_deps, engine = engine, afp_root = afp_root,
-            build_hosts = build_hosts, hostname = hostname(build_options), build_heap = build_heap,
+            build_hosts = build_hosts, hostname = hostname(build_options),
+            clean_sessions = clean_sessions, build_heap = build_heap,
             numa_shuffling = numa_shuffling, fresh_build = fresh_build,
             no_build = no_build, session_setup = session_setup,
             jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true)
 
-        if (clean_build) {
-          for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
-            store.clean_output(database_server, name, progress = progress)
-          }
-        }
-
         val results = engine.run_build_process(build_context, progress, server)
 
         if (export_files) {
diff -r 90fbcdafb34e -r 32ca3d1283de src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Thu Feb 22 21:03:55 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Thu Feb 22 21:28:55 2024 +0100
@@ -1107,6 +1107,15 @@
   }
 
 
+  /* prepare */
+
+  def prepare(): Unit = {
+    for (name <- build_context.clean_sessions) {
+      store.clean_output(_database_server, name, progress = progress)
+    }
+  }
+
+
   /* run */
 
   def run(): Build.Results = {