diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Tue Nov 04 21:49:24 2025 +0100 +++ b/src/Pure/Build/build_job.scala Tue Nov 04 22:09:26 2025 +0100 @@ -160,6 +160,7 @@ private def nodes_status_progress(state: Document.State = get_state()): Unit = { val result = synchronized { + lazy val now = progress.now() for (id <- state.progress_theories if !nodes_changed(id)) nodes_changed += id val nodes_status1 = nodes_changed.foldLeft(nodes_status)({ case (status, state_id) => @@ -167,7 +168,7 @@ case None => status case Some(snapshot) => Exn.Interrupt.expose() - status.update_node(progress.now(), + status.update_node(now, snapshot.state, snapshot.version, snapshot.node_name, threshold = editor_timing_threshold) } @@ -175,7 +176,7 @@ val result = if (nodes_changed.isEmpty) None else { - Some(Progress.Nodes_Status( + Some(Progress.Nodes_Status(now, nodes_domain, nodes_status1, session = resources.session_background.session_name, old = Some(nodes_status)))