# HG changeset patch
# User wenzelm
# Date 1454617373 -3600
# Node ID 8bf765c9c2e54eb8d60270cfed2db5a6c5fc94a6
# Parent  74dc98bd9f51d5bb1397b690e1764b4542d059c0
separate delay_repaint to ensure reactivity, indepently of future_refresh status;
clarified delay_refresh: do not cancel already running task, but retry later;

diff -r 74dc98bd9f51 -r 8bf765c9c2e5 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Feb 04 16:30:01 2016 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Feb 04 21:22:53 2016 +0100
@@ -72,6 +72,9 @@
   private var current_overview = Overview()
   private var current_colors: List[(Color, Int, Int)] = Nil
 
+  private val delay_repaint =
+    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
+
   override def paintComponent(gfx: Graphics)
   {
     super.paintComponent(gfx)
@@ -83,7 +86,7 @@
         val overview = get_overview()
 
         if (rendering.snapshot.is_outdated || overview != current_overview) {
-          invoke()
+          delay_repaint.invoke()
 
           gfx.setColor(rendering.outdated_color)
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
@@ -103,23 +106,21 @@
 
   /* asynchronous refresh */
 
-  private var future_refresh: Option[Future[Unit]] = None
-  private def cancel(): Unit = future_refresh.map(_.cancel)
+  private val future_refresh = Synchronized(Future.value(()))
+  private def is_running(): Boolean = !future_refresh.value.is_finished
 
   def invoke(): Unit = delay_refresh.invoke()
-  def revoke(): Unit = delay_refresh.revoke()
+  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
 
   private val delay_refresh =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
+    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
       doc_view.rich_text_area.robust_body(()) {
         JEdit_Lib.buffer_lock(buffer) {
           val rendering = doc_view.get_rendering()
           val overview = get_overview()
 
-          if (rendering.snapshot.is_outdated) invoke()
+          if (rendering.snapshot.is_outdated || is_running()) invoke()
           else {
-            cancel()
-
             val line_offsets =
             {
               val line_manager = JEdit_Lib.buffer_line_manager(buffer)
@@ -128,8 +129,8 @@
               a
             }
 
-            future_refresh =
-              Some(Future.fork {
+            future_refresh.change(_ =>
+              Future.fork {
                 val line_count = overview.line_count
                 val char_count = overview.char_count
                 val L = overview.L
@@ -170,7 +171,8 @@
                   current_colors = new_colors
                   repaint()
                 }
-              })
+              }
+            )
           }
         }
       }