tuned;
authorwenzelm
Sun, 08 Jan 2017 17:10:42 +0100
changeset 64836 3611f759f896
parent 64835 fd1efd6dd385
child 64837 4efe34df9136
tuned;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.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 =
--- 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()