src/Pure/Build/build_job.scala
changeset 83315 03dfb684a50d
parent 83313 73abc1020bfd
child 83503 7b1b7ac616c0
--- a/src/Pure/Build/build_job.scala	Sun Oct 19 13:45:07 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sun Oct 19 14:05:58 2025 +0200
@@ -191,9 +191,10 @@
     private lazy val nodes_delay: Delay =
       Delay.first(build_progress_delay) { nodes_status_progress(); nodes_delay.invoke() }
 
-    def nodes_status_sync(state: Document.State): Unit = {
+    def nodes_status_exit(state: Document.State): Unit = synchronized {
       nodes_delay.revoke()
       nodes_status_progress(state = state)
+      progress.nodes_status(Progress.Nodes_Status.empty(resources.session_background.session_name))
     }
 
     override def start(start_prover: Prover.Receiver => Prover): Unit = {
@@ -328,7 +329,7 @@
 
           session.init_protocol_handler(new Session.Protocol_Handler {
               override def exit(exit_state: Document.State): Unit = {
-                session.nodes_status_sync(exit_state)
+                session.nodes_status_exit(exit_state)
                 session.errors_cancel()
               }