src/Tools/jEdit/src/jedit_resources.scala
changeset 64813 7283f41d05ab
parent 64797 891a25a87ea1
child 64834 0a7179ad430d
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Jan 06 11:58:29 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Jan 06 13:27:18 2017 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4          val changed = change.syntax_changed.toSet
     1.5          for {
     1.6            buffer <- JEdit_Lib.jedit_buffers()
     1.7 -          model <- PIDE.document_model(buffer)
     1.8 +          model <- Document_Model.get(buffer)
     1.9            if changed(model.node_name)
    1.10          } model.syntax_changed()
    1.11        }