# HG changeset patch
# User wenzelm
# Date 1353943349 -3600
# Node ID de77cde5737658374ac3ea4e8c535858f3d64233
# Parent  97959912840a71562867dac7952a4df208429c40
reset active areas on content update;

diff -r 97959912840a -r de77cde57376 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 16:22:29 2012 +0100
@@ -93,6 +93,7 @@
           Swing_Thread.later {
             current_rendering = rendering
             JEdit_Lib.buffer_edit(getBuffer) {
+              rich_text_area.active_reset()
               getBuffer.setReadOnly(false)
               setText(text)
               setCaretPosition(0)
diff -r 97959912840a -r de77cde57376 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:22:29 2012 +0100
@@ -138,7 +138,7 @@
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
-  private def active_reset(): Unit = active_areas.foreach(_._1.reset)
+  def active_reset(): Unit = active_areas.foreach(_._1.reset)
 
   private val focus_listener = new FocusAdapter {
     override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }