src/Pure/Build/build_job.scala
changeset 83507 989304e45ad7
parent 83504 24998f6c9c15
--- 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)))