--- 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()