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()
     }