tuned;
authorwenzelm
Sat, 28 Jun 2025 17:12:41 +0200
changeset 82792 d3f0f72b2c43
parent 82791 57527794c788
child 82793 fe8598c92be7
tuned;
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))
               }