--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Dec 02 14:16:56 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Dec 02 16:10:11 2014 +0100
@@ -114,7 +114,15 @@
override def commit(change: Session.Change)
{
- if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
+ if (!change.syntax_changed.isEmpty)
+ GUI_Thread.later {
+ val changed = change.syntax_changed.toSet
+ for {
+ buffer <- JEdit_Lib.jedit_buffers()
+ model <- PIDE.document_model(buffer)
+ if changed(model.node_name)
+ } model.syntax_changed()
+ }
if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
}
}