# HG changeset patch
# User wenzelm
# Date 1751123561 -7200
# Node ID d3f0f72b2c436a2db2f2ef95f9bb66f4329457e0
# Parent  57527794c7888f732c8341e09b30e1705f3370ec
tuned;

diff -r 57527794c788 -r d3f0f72b2c43 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 16:24:58 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 17:12:41 2025 +0200
@@ -169,7 +169,8 @@
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
     commands: Linear_Set[Command],
-    first: Command, last: Command
+    first: Command,
+    last: Command
   ): Linear_Set[Command] = {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
@@ -345,7 +346,7 @@
               edits.foldLeft(node1)(
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
-              if (reparse_set.contains(name)) {
+              if (reparse_set(name)) {
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit,
                   node2, (name, node2.edit_perspective))
               }