# HG changeset patch
# User wenzelm
# Date 1446457122 -3600
# Node ID bf4969660913658153c4e17e530a2f69c02683c4
# Parent  f6bd97a587b7260805ad204623af0a1f18764eda
avoid highlighted area getting "stuck" after edit;

diff -r f6bd97a587b7 -r bf4969660913 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 02 10:20:27 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 02 10:38:42 2015 +0100
@@ -255,6 +255,9 @@
       reset_blob()
       reset_bibtex()
 
+      for (doc_view <- PIDE.document_views(buffer))
+        doc_view.rich_text_area.active_reset()
+
       if (clear) {
         pending_clear = true
         pending.clear