tuned;
authorwenzelm
Sun Jan 08 17:10:42 2017 +0100 (2017-01-08 ago)
changeset 648363611f759f896
parent 64835 fd1efd6dd385
child 64837 4efe34df9136
tuned;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 16:47:53 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 17:10:42 2017 +0100
     1.3 @@ -87,6 +87,19 @@
     1.4      } yield Text.Info(range, (entry, model))
     1.5  
     1.6  
     1.7 +  /* syntax */
     1.8 +
     1.9 +  def syntax_changed(names: List[Document.Node.Name])
    1.10 +  {
    1.11 +    GUI_Thread.require {}
    1.12 +
    1.13 +    val models = state.value.models
    1.14 +    for (name <- names.iterator; model <- models.get(name)) {
    1.15 +      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
    1.16 +    }
    1.17 +  }
    1.18 +
    1.19 +
    1.20    /* init and exit */
    1.21  
    1.22    def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 16:47:53 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:10:42 2017 +0100
     2.3 @@ -124,14 +124,7 @@
     2.4    override def commit(change: Session.Change)
     2.5    {
     2.6      if (change.syntax_changed.nonEmpty)
     2.7 -      GUI_Thread.later {
     2.8 -        val changed = change.syntax_changed.toSet
     2.9 -        for {
    2.10 -          buffer <- JEdit_Lib.jedit_buffers()
    2.11 -          model <- Document_Model.get(buffer)
    2.12 -          if changed(model.node_name)
    2.13 -        } model.syntax_changed()
    2.14 -      }
    2.15 +      GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
    2.16      if (change.deps_changed ||
    2.17          PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
    2.18        PIDE.deps_changed()