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