# HG changeset patch
# User wenzelm
# Date 1750675373 -7200
# Node ID 4694d8cce777feb5a1c806274f0b1d22214839d4
# Parent  89347c0cc6a391a0a8a23d8ffe99d43910966e62
tuned;

diff -r 89347c0cc6a3 -r 4694d8cce777 src/Tools/jEdit/src/document_model.scala
--- 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()
   }