# HG changeset patch
# User wenzelm
# Date 1666001723 -7200
# Node ID 43e66527fa93e78e5d275f46505605b8e0bd2600
# Parent  3e1e2f9198bb2511c5f1ef40524d79af00084b18
tuned signature;

diff -r 3e1e2f9198bb -r 43e66527fa93 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Oct 17 11:58:13 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Oct 17 12:15:23 2022 +0200
@@ -255,7 +255,7 @@
     def flush(): Unit = synchronized {
       if (assignment || nodes.nonEmpty || commands.nonEmpty)
         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
-      if (nodes.nonEmpty) consolidation.update(nodes)
+      if (nodes.nonEmpty) consolidation.update(more_nodes = nodes)
       assignment = false
       nodes = Set.empty
       commands = Set.empty
@@ -312,10 +312,10 @@
       state.change(_ => None)
     }
 
-    def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit = {
+    def update(more_nodes: Set[Document.Node.Name] = Set.empty): Unit = {
       val active =
         state.change_result(st =>
-          (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
+          (st.isDefined, st.map(nodes => if (nodes.isEmpty) more_nodes else nodes ++ more_nodes)))
       if (active) delay.invoke()
     }