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