# HG changeset patch
# User wenzelm
# Date 1483891842 -3600
# Node ID 3611f759f89692a6fc80a8bf44a5fa90b7ab46c2
# Parent  fd1efd6dd385f839120b202e260d56a426ea65f4
tuned;

diff -r fd1efd6dd385 -r 3611f759f896 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 16:47:53 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 17:10:42 2017 +0100
@@ -87,6 +87,19 @@
     } yield Text.Info(range, (entry, model))
 
 
+  /* syntax */
+
+  def syntax_changed(names: List[Document.Node.Name])
+  {
+    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 _ => }
+    }
+  }
+
+
   /* init and exit */
 
   def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
diff -r fd1efd6dd385 -r 3611f759f896 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 16:47:53 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:10:42 2017 +0100
@@ -124,14 +124,7 @@
   override def commit(change: Session.Change)
   {
     if (change.syntax_changed.nonEmpty)
-      GUI_Thread.later {
-        val changed = change.syntax_changed.toSet
-        for {
-          buffer <- JEdit_Lib.jedit_buffers()
-          model <- Document_Model.get(buffer)
-          if changed(model.node_name)
-        } model.syntax_changed()
-      }
+      GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
     if (change.deps_changed ||
         PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
       PIDE.deps_changed()