reset active areas on content update;

--- 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)

--- 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() } }