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