# HG changeset patch
# User wenzelm
# Date 1461069535 -7200
# Node ID 5fb352275db3fcff7feea7099be3cbc57034fc5c
# Parent  785a59235a1502c0a26eafded008de1aca9a2165
more thorough update;

diff -r 785a59235a15 -r 5fb352275db3 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 19 12:06:34 2016 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 19 14:38:55 2016 +0200
@@ -63,8 +63,8 @@
   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
 
   val rich_text_area =
-    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
-      () => None, caret_visible = true, enable_hovering = false)
+    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
+      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
 
 
   /* perspective */
diff -r 785a59235a15 -r 5fb352275db3 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 19 12:06:34 2016 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 19 14:38:55 2016 +0200
@@ -81,7 +81,7 @@
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
-      get_search_pattern _, caret_visible = false, enable_hovering = true)
+      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
 
   private var current_search_pattern: Option[Regex] = None
   def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
diff -r 785a59235a15 -r 5fb352275db3 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 19 12:06:34 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 19 14:38:55 2016 +0200
@@ -32,6 +32,7 @@
   get_rendering: () => Rendering,
   close_action: () => Unit,
   get_search_pattern: () => Option[Regex],
+  caret_update: () => Unit,
   caret_visible: Boolean,
   enable_hovering: Boolean)
 {
@@ -129,6 +130,7 @@
         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
 
       if (new_text_info != old_text_info) {
+        caret_update()
         if (cursor.isDefined) {
           if (new_text_info.isDefined)
             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))