# HG changeset patch
# User wenzelm
# Date 1671805253 -3600
# Node ID 9766a2a571827a88bf14f25cac68c808f788fdbf
# Parent  35f41096de36a15dd09d26ece736947afc611f1a
tuned;

diff -r 35f41096de36 -r 9766a2a57182 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 23 15:07:48 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 23 15:20:53 2022 +0100
@@ -1079,11 +1079,11 @@
           commands.get(command.id).foreach(st => commands1 += (command.id -> st))
         }
 
-        for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
-          if (!execs1.isDefinedAt(exec_id)) {
-            execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
-          }
-        }
+        for {
+          exec_id <- command_execs.getOrElse(command.id, Nil)
+          if !execs1.isDefinedAt(exec_id)
+          st <- execs.get(exec_id)
+        } execs1 += (exec_id -> st)
       }
 
       copy(