avoid shortcuts based on potentially expensive equality test;

--- a/src/Pure/Build/build_job.scala	Mon Sep 22 16:43:53 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Mon Sep 22 17:20:06 2025 +0200
@@ -237,10 +237,10 @@
                     }
                   }
                 )
-                val updated = nodes_status1 != nodes_status
+                val changed = nodes_changed.nonEmpty
                 nodes_changed = Set.empty
                 nodes_status = nodes_status1
-                if (updated) Some(Progress.Nodes_Status(nodes_domain, nodes_status1)) else None
+                if (changed) Some(Progress.Nodes_Status(nodes_domain, nodes_status1)) else None
               }
             result.foreach(progress.nodes_status)
           }

--- a/src/Pure/PIDE/document_status.scala	Mon Sep 22 16:43:53 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Sep 22 17:20:06 2025 +0200
@@ -346,9 +346,8 @@
       name: Document.Node.Name,
       threshold: Time = Time.max
     ): Nodes_Status = {
-      val st = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
-      if (apply(name) == st) this
-      else new Nodes_Status(rep + (name -> st))
+      val node_status = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
+      new Nodes_Status(rep + (name -> node_status))
     }
 
     def update_nodes(