# HG changeset patch
# User paulson
# Date 1672854387 0
# Node ID 97a11357485c0393031e36e705dc418607639dc7
# Parent  7c3d50ffaecee134324051d938b6b75631f745b1# Parent  969913b19a935193b3f4d77ca6be4b2878cd51f4
merged

diff -r 969913b19a93 -r 97a11357485c src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 10:27:32 2023 +0000
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 04 17:46:27 2023 +0000
@@ -19,8 +19,9 @@
     perspective: Text.Perspective,
     overlays: Document.Node.Overlays
   ): (Command.Perspective, Command.Perspective) = {
-    if (perspective.is_empty && overlays.is_empty)
+    if (perspective.is_empty && overlays.is_empty) {
       (Command.Perspective.empty, Command.Perspective.empty)
+    }
     else {
       val has_overlay = overlays.commands
       val visible = new mutable.ListBuffer[Command]
@@ -215,7 +216,8 @@
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,
-    node: Document.Node, edit: Document.Edit_Text
+    node: Document.Node,
+    edit: Document.Edit_Text
   ): Document.Node = {
     /* recover command spans after edits */
     // FIXME somewhat slow
@@ -313,8 +315,9 @@
         val reparse =
           nodes0.iterator.foldLeft(syntax_changed) {
             case (reparse, (name, node)) =>
-              if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
+              if (node.load_commands_changed(doc_blobs) && !reparse.contains(name)) {
                 name :: reparse
+              }
               else reparse
           }
         val reparse_set = reparse.toSet
@@ -333,22 +336,25 @@
             val commands = node.commands
 
             val node1 =
-              if (reparse_set(name) && commands.nonEmpty)
+              if (reparse_set(name) && commands.nonEmpty) {
                 node.update_commands(
                   reparse_spans(resources, syntax, get_blob, can_import, name,
                     commands, commands.head, commands.last))
+              }
               else node
             val node2 =
               edits.foldLeft(node1)(
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
-              if (reparse_set.contains(name))
+              if (reparse_set.contains(name)) {
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit,
                   node2, (name, node2.edit_perspective))
+              }
               else node2
 
-            if (!node.same_perspective(node3.text_perspective, node3.perspective))
+            if (!node.same_perspective(node3.text_perspective, node3.perspective)) {
               doc_edits += (name -> node3.perspective)
+            }
 
             doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))