clarified signature;

--- a/src/Pure/PIDE/document_status.scala	Sun Sep 21 19:39:52 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Sep 21 19:47:26 2025 +0200
@@ -291,7 +291,18 @@
         case _ => Overall_Status.pending
       }
 
-    def update(
+    def update_node(
+      state: Document.State,
+      version: Document.Version,
+      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))
+    }
+
+    def update_nodes(
       resources: Resources,
       state: Document.State,
       version: Document.Version,
@@ -299,16 +310,14 @@
       domain: Option[Set[Document.Node.Name]] = None,
       trim: Boolean = false
     ): Nodes_Status = {
-      val nodes1 = version.nodes
-      val update_iterator =
-        for {
-          name <- domain.getOrElse(nodes1.domain).iterator
-          if !Resources.hidden_node(name) && !resources.loaded_theory(name)
-          st = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
-          if apply(name) != st
-        } yield (name -> st)
-      val rep1 = rep ++ update_iterator
-      new Nodes_Status(if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1)
+      val domain1 = version.nodes.domain
+      val that =
+        domain.getOrElse(domain1).iterator.foldLeft(this)(
+          { case (a, name) =>
+              if (Resources.hidden_node(name) || resources.loaded_theory(name)) a
+              else a.update_node(state, version, name, threshold = threshold) })
+      if (trim) new Nodes_Status(that.rep -- that.rep.keysIterator.filterNot(domain1))
+      else that
     }
 
     override def hashCode: Int = rep.hashCode

--- a/src/Pure/PIDE/headless.scala	Sun Sep 21 19:39:52 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 21 19:47:26 2025 +0200
@@ -141,7 +141,7 @@
         trim: Boolean = false
       ): (Boolean, Use_Theories_State) = {
         val nodes_status1 =
-          nodes_status.update(resources, state, version, domain = domain, trim = trim)
+          nodes_status.update_nodes(resources, state, version, domain = domain, trim = trim)
         val st1 = copy(last_update = Time.now(), nodes_status = nodes_status1)
         (nodes_status1 != nodes_status, st1)
       }

--- a/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 19:39:52 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 19:47:26 2025 +0200
@@ -236,7 +236,7 @@
     val snapshot = PIDE.session.snapshot()
 
     val nodes_status1 =
-      nodes_status.update(
+      nodes_status.update_nodes(
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     if (force || nodes_status1 != nodes_status) {

--- a/src/Tools/jEdit/src/timing_dockable.scala	Sun Sep 21 19:39:52 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Sun Sep 21 19:47:26 2025 +0200
@@ -166,7 +166,7 @@
           .filterNot(PIDE.resources.loaded_theory).toSet)
 
     nodes_status =
-      nodes_status.update(PIDE.resources, snapshot.state, snapshot.version,
+      nodes_status.update_nodes(PIDE.resources, snapshot.state, snapshot.version,
         threshold = Time.seconds(timing_threshold),
         domain = Some(domain))