reset active areas on content update;
authorwenzelm
Mon Nov 26 16:22:29 2012 +0100 (2012-11-26 ago)
changeset 50216de77cde57376
parent 50215 97959912840a
child 50217 ce1f0602f48e
reset active areas on content update;
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 16:22:29 2012 +0100
     1.3 @@ -93,6 +93,7 @@
     1.4            Swing_Thread.later {
     1.5              current_rendering = rendering
     1.6              JEdit_Lib.buffer_edit(getBuffer) {
     1.7 +              rich_text_area.active_reset()
     1.8                getBuffer.setReadOnly(false)
     1.9                setText(text)
    1.10                setCaretPosition(0)
     2.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:22:29 2012 +0100
     2.3 @@ -138,7 +138,7 @@
     2.4  
     2.5    private val active_areas =
     2.6      List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
     2.7 -  private def active_reset(): Unit = active_areas.foreach(_._1.reset)
     2.8 +  def active_reset(): Unit = active_areas.foreach(_._1.reset)
     2.9  
    2.10    private val focus_listener = new FocusAdapter {
    2.11      override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }