tuned;
authorwenzelm
Fri, 23 Dec 2022 15:07:48 +0100
changeset 76759 35f41096de36
parent 76758 8fc7157485d8
child 76760 9766a2a57182
tuned;
src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 23 14:43:04 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 23 15:07:48 2022 +0100
@@ -319,9 +319,10 @@
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else
+      else {
         new Node(get_blob, header, syntax, text_perspective, perspective,
           Node.Commands(new_commands))
+      }
 
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)
@@ -993,9 +994,12 @@
       val edited_nodes =
         (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
 
-      def upd(exec_id: Document_ID.Exec, st: Command.State)
-          : Option[(Document_ID.Exec, Command.State)] =
+      def upd(
+        exec_id: Document_ID.Exec,
+        st: Command.State
+      ): Option[(Document_ID.Exec, Command.State)] = {
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
+      }
 
       val (changed_commands, new_execs) =
         update.foldLeft((List.empty[Command], execs)) {
@@ -1071,12 +1075,14 @@
           blobs1 += digest
         }
 
-        if (!commands1.isDefinedAt(command.id))
+        if (!commands1.isDefinedAt(command.id)) {
           commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+        }
 
         for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
-          if (!execs1.isDefinedAt(exec_id))
+          if (!execs1.isDefinedAt(exec_id)) {
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
+          }
         }
       }