src/Tools/jEdit/src/jedit_resources.scala
changeset 59078 cf255dc2b48f
parent 59077 7e0d3da6e6d8
child 59319 677615cba30d
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 14:16:56 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 16:10:11 2014 +0100
     1.3 @@ -114,7 +114,15 @@
     1.4  
     1.5    override def commit(change: Session.Change)
     1.6    {
     1.7 -    if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
     1.8 +    if (!change.syntax_changed.isEmpty)
     1.9 +      GUI_Thread.later {
    1.10 +        val changed = change.syntax_changed.toSet
    1.11 +        for {
    1.12 +          buffer <- JEdit_Lib.jedit_buffers()
    1.13 +          model <- PIDE.document_model(buffer)
    1.14 +          if changed(model.node_name)
    1.15 +        } model.syntax_changed()
    1.16 +      }
    1.17      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
    1.18    }
    1.19  }