# HG changeset patch # User wenzelm # Date 1442687908 -7200 # Node ID 42419fe6f66049b781e2efa347463c52e4a269f0 # Parent e4699ef5cf908b723ae9e62b042e19120571c08b fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy; diff -r e4699ef5cf90 -r 42419fe6f660 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sat Sep 19 20:31:57 2015 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Sat Sep 19 20:38:28 2015 +0200 @@ -194,19 +194,14 @@ /* text status overview left of scrollbar */ - private object overview extends Text_Overview(this) - { - val delay_repaint = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() } - } + private val overview = new Text_Overview(this) /* main */ private val main = Session.Consumer[Any](getClass.getName) { - case _: Session.Raw_Edits => - overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay")) + case _: Session.Raw_Edits => overview.postpone() case changed: Session.Commands_Changed => val buffer = model.buffer @@ -221,7 +216,7 @@ if (changed.assignment || load_changed || (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) - overview.delay_repaint.invoke() + overview.invoke() val visible_lines = text_area.getVisibleLines if (visible_lines > 0) { @@ -275,7 +270,7 @@ session.commands_changed -= main Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). foreach(text_area.removeStructureMatcher(_)) - text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke() + text_area.removeLeftOfScrollBar(overview); overview.revoke() text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() text_area.removeKeyListener(key_listener) text_area.getGutter.removeExtension(gutter_painter) diff -r e4699ef5cf90 -r 42419fe6f660 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Sat Sep 19 20:31:57 2015 +0200 +++ b/src/Tools/jEdit/src/text_overview.scala Sat Sep 19 20:38:28 2015 +0200 @@ -11,6 +11,7 @@ import scala.annotation.tailrec +import java.util.concurrent.{Future => JFuture} import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color} import java.awt.event.{MouseAdapter, MouseEvent} import javax.swing.{JPanel, ToolTipManager} @@ -18,14 +19,16 @@ class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout) { + /* GUI components */ + private val text_area = doc_view.text_area private val buffer = doc_view.model.buffer + private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines + private val WIDTH = 10 private val HEIGHT = 4 - private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines - setPreferredSize(new Dimension(WIDTH, 0)) setRequestFocusEnabled(false) @@ -49,17 +52,44 @@ } - /* painting based on cached result */ + /* overview */ - private var cached_colors: List[(Color, Int, Int)] = Nil + private case class Overview( + relevant_range: Text.Range = Text.Range(0), + line_count: Int = 0, + char_count: Int = 0, + L: Int = 0, + H: Int = 0) - private var last_snapshot = Document.Snapshot.init - private var last_options = PIDE.options.value - private var last_relevant_range = Text.Range(0) - private var last_line_count = 0 - private var last_char_count = 0 - private var last_L = 0 - private var last_H = 0 + private def get_overview(rendering: Rendering): Overview = + { + val char_count = buffer.getLength + Overview( + relevant_range = + JEdit_Lib.visible_range(text_area) match { + case None => Text.Range(0) + case Some(visible_range) => + val len = rendering.overview_limit max visible_range.length + val start = (visible_range.start + visible_range.stop - len) / 2 + val stop = start + len + + if (start < 0) Text.Range(0, len min char_count) + else if (stop > char_count) Text.Range((char_count - len) max 0, char_count) + else Text.Range(start, stop) + }, + line_count = buffer.getLineCount, + char_count = char_count, + L = lines(), + H = getHeight()) + } + + + /* synchronous painting */ + + private var current_snapshot = Document.Snapshot.init + private var current_options = PIDE.options.value + private var current_overview = Overview() + private var current_colors: List[(Color, Int, Int)] = Nil override def paintComponent(gfx: Graphics) { @@ -71,86 +101,110 @@ val rendering = doc_view.get_rendering() val snapshot = rendering.snapshot val options = rendering.options + val overview = get_overview(rendering) - if (snapshot.is_outdated) { - gfx.setColor(rendering.outdated_color) - gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) - } - else { + if (!snapshot.is_outdated && overview == current_overview) { gfx.setColor(getBackground) gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) - - val line_count = buffer.getLineCount - val char_count = buffer.getLength - - val L = lines() - val H = getHeight() - - val relevant_range = - JEdit_Lib.visible_range(text_area) match { - case None => Text.Range(0) - case Some(visible_range) => - val len = rendering.overview_limit max visible_range.length - val start = (visible_range.start + visible_range.stop - len) / 2 - val stop = start + len - - if (start < 0) Text.Range(0, len min char_count) - else if (stop > char_count) Text.Range((char_count - len) max 0, char_count) - else Text.Range(start, stop) - } - - if (!(line_count == last_line_count && char_count == last_char_count && - L == last_L && H == last_H && relevant_range == last_relevant_range && - (snapshot eq_content last_snapshot) && (options eq last_options))) - { - @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) - : List[(Color, Int, Int)] = - { - if (l < line_count && h < H) { - val p1 = p + H - val q1 = q + HEIGHT * L - val (l1, h1) = - if (p1 >= q1) (l + 1, h + (p1 - q) / L) - else (l + (q1 - p) / H, h + HEIGHT) - - val start = buffer.getLineStartOffset(l) - val end = - if (l1 < line_count) buffer.getLineStartOffset(l1) - else char_count - val range = Text.Range(start, end) - - val range_color = - if (range overlaps relevant_range) rendering.overview_color(range) - else Some(rendering.outdated_color) - val colors1 = - (range_color, colors) match { - case (Some(color), (old_color, old_h, old_h1) :: rest) - if color == old_color && old_h1 == h => (color, old_h, h1) :: rest - case (Some(color), _) => (color, h, h1) :: colors - case (None, _) => colors - } - loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1) - } - else colors.reverse - } - cached_colors = loop(0, 0, 0, 0, Nil) - - last_snapshot = snapshot - last_options = options - last_relevant_range = relevant_range - last_line_count = line_count - last_char_count = char_count - last_L = L - last_H = H - } - - for ((color, h, h1) <- cached_colors) { + for ((color, h, h1) <- current_colors) { gfx.setColor(color) gfx.fillRect(0, h, getWidth, h1 - h) } } + else { + gfx.setColor(rendering.outdated_color) + gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) + } } } } + + + /* asynchronous refresh */ + + private var future_refresh: Option[JFuture[Unit]] = None + private def cancel(): Unit = future_refresh.map(_.cancel(true)) + + def invoke(): Unit = delay_refresh.invoke() + def revoke(): Unit = delay_refresh.revoke() + def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) } + + private val delay_refresh = + GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) { + doc_view.rich_text_area.robust_body(()) { + JEdit_Lib.buffer_lock(buffer) { + val rendering = doc_view.get_rendering() + val snapshot = rendering.snapshot + val options = rendering.options + val overview = get_overview(rendering) + + if (!snapshot.is_outdated && + (overview != current_overview || + !(snapshot eq_content current_snapshot) || + !(options eq current_options))) + { + cancel() + + val line_offsets = + { + val line_manager = JEdit_Lib.buffer_line_manager(buffer) + val a = new Array[Int](line_manager.getLineCount) + for (i <- 1 until a.length) a(i) = line_manager.getLineEndOffset(i - 1) + a + } + + future_refresh = + Some(Simple_Thread.submit_task { + val relevant_range = overview.relevant_range + val line_count = overview.line_count + val char_count = overview.char_count + val L = overview.L + val H = overview.H + + @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) + : List[(Color, Int, Int)] = + { + Exn.Interrupt.expose() + + if (l < line_count && h < H) { + val p1 = p + H + val q1 = q + HEIGHT * L + val (l1, h1) = + if (p1 >= q1) (l + 1, h + (p1 - q) / L) + else (l + (q1 - p) / H, h + HEIGHT) + + val start = line_offsets(l) + val end = + if (l1 < line_count) line_offsets(l1) + else char_count + val range = Text.Range(start, end) + + val range_color = + if (range overlaps relevant_range) rendering.overview_color(range) + else Some(rendering.outdated_color) + val colors1 = + (range_color, colors) match { + case (Some(color), (old_color, old_h, old_h1) :: rest) + if color == old_color && old_h1 == h => (color, old_h, h1) :: rest + case (Some(color), _) => (color, h, h1) :: colors + case (None, _) => colors + } + loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1) + } + else colors.reverse + } + val new_colors = loop(0, 0, 0, 0, Nil) + + GUI_Thread.later { + current_snapshot = snapshot + current_options = options + current_overview = overview + current_colors = new_colors + repaint() + } + }) + } + } + } + } } -