more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
authorwenzelm
Tue Dec 02 16:10:11 2014 +0100 (2014-12-02)
changeset 59078cf255dc2b48f
parent 59077 7e0d3da6e6d8
child 59079 12a689755c3d
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 14:16:56 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:10:11 2014 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  import org.gjt.sp.jedit.jEdit
     1.6  import org.gjt.sp.jedit.Buffer
     1.7 -import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
     1.8 +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer, LineManager}
     1.9  
    1.10  
    1.11  object Document_Model
    1.12 @@ -284,28 +284,42 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* activation */
    1.17 +  /* syntax */
    1.18  
    1.19 -  private def refresh_token_marker()
    1.20 +  def syntax_changed()
    1.21 +  {
    1.22 +    Untyped.get(buffer, "lineMgr").asInstanceOf[LineManager].setFirstInvalidLineContext(0)
    1.23 +    for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
    1.24 +      val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea")
    1.25 +      val m = c.getDeclaredMethod("foldStructureChanged")
    1.26 +      m.setAccessible(true)
    1.27 +      m.invoke(text_area)
    1.28 +    }
    1.29 +  }
    1.30 +
    1.31 +  private def init_token_marker()
    1.32    {
    1.33      Isabelle.buffer_token_marker(buffer) match {
    1.34        case Some(marker) if marker != buffer.getTokenMarker =>
    1.35 -        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    1.36          buffer.setTokenMarker(marker)
    1.37 +        syntax_changed()
    1.38        case _ =>
    1.39      }
    1.40    }
    1.41  
    1.42 +
    1.43 +  /* activation */
    1.44 +
    1.45    private def activate()
    1.46    {
    1.47      pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
    1.48      buffer.addBufferListener(buffer_listener)
    1.49 -    refresh_token_marker()
    1.50 +    init_token_marker()
    1.51    }
    1.52  
    1.53    private def deactivate()
    1.54    {
    1.55      buffer.removeBufferListener(buffer_listener)
    1.56 -    refresh_token_marker()
    1.57 +    init_token_marker()
    1.58    }
    1.59  }
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 14:16:56 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 16:10:11 2014 +0100
     2.3 @@ -114,7 +114,15 @@
     2.4  
     2.5    override def commit(change: Session.Change)
     2.6    {
     2.7 -    if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
     2.8 +    if (!change.syntax_changed.isEmpty)
     2.9 +      GUI_Thread.later {
    2.10 +        val changed = change.syntax_changed.toSet
    2.11 +        for {
    2.12 +          buffer <- JEdit_Lib.jedit_buffers()
    2.13 +          model <- PIDE.document_model(buffer)
    2.14 +          if changed(model.node_name)
    2.15 +        } model.syntax_changed()
    2.16 +      }
    2.17      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
    2.18    }
    2.19  }