clarified signature: prefer explicit operations;

--- a/src/Pure/PIDE/document_status.scala	Sun Sep 21 14:22:14 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Sep 21 14:28:42 2025 +0200
@@ -298,7 +298,7 @@
       threshold: Time = Time.max,
       domain: Option[Set[Document.Node.Name]] = None,
       trim: Boolean = false
-    ): (Boolean, Nodes_Status) = {
+    ): Nodes_Status = {
       val nodes1 = version.nodes
       val update_iterator =
         for {
@@ -308,9 +308,7 @@
           if apply(name) != st
         } yield (name -> st)
       val rep1 = rep ++ update_iterator
-      val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
-
-      (rep != rep2, new Nodes_Status(rep2))
+      new Nodes_Status(if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1)
     }
 
     override def hashCode: Int = rep.hashCode

--- a/src/Pure/PIDE/headless.scala	Sun Sep 21 14:22:14 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 21 14:28:42 2025 +0200
@@ -140,10 +140,10 @@
         domain: Option[Set[Document.Node.Name]] = None,
         trim: Boolean = false
       ): (Boolean, Use_Theories_State) = {
-        val (nodes_status_changed, nodes_status1) =
+        val nodes_status1 =
           nodes_status.update(resources, state, version, domain = domain, trim = trim)
         val st1 = copy(last_update = Time.now(), nodes_status = nodes_status1)
-        (nodes_status_changed, st1)
+        (nodes_status1 != nodes_status, st1)
       }
 
       def changed(

--- a/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 14:22:14 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 14:28:42 2025 +0200
@@ -235,12 +235,11 @@
 
     val snapshot = PIDE.session.snapshot()
 
-    val (nodes_status_changed, nodes_status1) =
+    val nodes_status1 =
       nodes_status.update(
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
-    nodes_status = nodes_status1
-    if (nodes_status_changed || force) {
+    if (force || nodes_status1 != nodes_status) {
       gui.listData =
         if (document) PIDE.editor.document_theories()
         else {
@@ -251,6 +250,8 @@
           } yield name).toList
         }
     }
+
+    nodes_status = nodes_status1
   }
 
 

--- a/src/Tools/jEdit/src/timing_dockable.scala	Sun Sep 21 14:22:14 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Sun Sep 21 14:28:42 2025 +0200
@@ -168,7 +168,7 @@
     nodes_status =
       nodes_status.update(PIDE.resources, snapshot.state, snapshot.version,
         threshold = Time.seconds(timing_threshold),
-        domain = Some(domain))._2
+        domain = Some(domain))
 
     val entries = make_entries()
     if (timing_view.listData.toList != entries) timing_view.listData = entries