src/Tools/jEdit/src/jedit_resources.scala
changeset 64836 3611f759f896
parent 64835 fd1efd6dd385
child 64837 4efe34df9136
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 16:47:53 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:10:42 2017 +0100
     1.3 @@ -124,14 +124,7 @@
     1.4    override def commit(change: Session.Change)
     1.5    {
     1.6      if (change.syntax_changed.nonEmpty)
     1.7 -      GUI_Thread.later {
     1.8 -        val changed = change.syntax_changed.toSet
     1.9 -        for {
    1.10 -          buffer <- JEdit_Lib.jedit_buffers()
    1.11 -          model <- Document_Model.get(buffer)
    1.12 -          if changed(model.node_name)
    1.13 -        } model.syntax_changed()
    1.14 -      }
    1.15 +      GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
    1.16      if (change.deps_changed ||
    1.17          PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
    1.18        PIDE.deps_changed()