src/Pure/Build/build_job.scala

--- a/src/Pure/Build/build_job.scala	Sat Oct 18 18:25:16 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sat Oct 18 21:20:30 2025 +0200
@@ -160,8 +160,7 @@
     private var nodes_changed = Set.empty[Document_ID.Generic]
     private var nodes_status = Document_Status.Nodes_Status.empty
 
-    private def nodes_status_progress(): Unit = {
-      val state = get_state()
+    private def nodes_status_progress(state: Document.State = get_state()): Unit = {
       val result =
         synchronized {
           for (id <- state.progress_theories if !nodes_changed(id)) nodes_changed += id
@@ -195,9 +194,9 @@
     private lazy val nodes_delay: Delay =
       Delay.first(build_progress_delay) { nodes_status_progress(); nodes_delay.invoke() }
 
-    def nodes_status_sync(): Unit = {
+    def nodes_status_sync(state: Document.State): Unit = {
       nodes_delay.revoke()
-      nodes_status_progress()
+      nodes_status_progress(state = state)
     }
 
     override def start(start_prover: Prover.Receiver => Prover): Unit = {
@@ -205,13 +204,6 @@
       super.start(start_prover)
     }
 
-    override def stop(): Process_Result = {
-      val result = super.stop()
-      nodes_status_sync()
-      stop_process_output()
-      result
-    }
-
     def command_timing(state_id: Document_ID.Generic, props: Properties.T): Unit = synchronized {
       val elapsed = Time.seconds(Markup.Elapsed.get(props))
       if (elapsed.is_notable(build_timing_threshold)) {
@@ -338,7 +330,10 @@
           }
 
           session.init_protocol_handler(new Session.Protocol_Handler {
-              override def exit(exit_state: Document.State): Unit = session.errors_cancel()
+              override def exit(exit_state: Document.State): Unit = {
+                session.nodes_status_sync(exit_state)
+                session.errors_cancel()
+              }
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean = {
                 val (rc, errors) =
@@ -444,7 +439,6 @@
                 session.synchronized { stderr ++= Symbol.encode(XML.content(message)) }
               }
               else if (msg.is_exit) {
-                session.nodes_status_sync()
                 val err =
                   "Prover terminated" +
                     (msg.properties match {
@@ -500,6 +494,7 @@
             }
 
           session.stop()
+          session.stop_process_output()
 
           val export_errors =
             export_consumer.shutdown(close = true).map(Output.error_message_text)