tuned;

--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 19 17:15:40 2025 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jun 23 12:42:53 2025 +0200
@@ -40,7 +40,7 @@
         (for {
           (node_name, model) <- models.iterator
           blob <- model.get_blob
-        } yield (node_name -> blob)).toMap)
+        } yield (node_name, blob)).toMap)
 
     def open_buffer(
       session: Session,
@@ -139,9 +139,10 @@
     GUI_Thread.require {}
 
     val models = state.value.models
-    for (name <- names.iterator; model <- models.get(name)) {
-      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
-    }
+    for {
+      name <- names.iterator
+      case buffer_model: Buffer_Model <- models.get(name)
+    } buffer_model.syntax_changed()
   }