# HG changeset patch # User wenzelm # Date 1442688431 -7200 # Node ID 67c20ce71d22516ea90b2960154af7abefed1134 # Parent 42419fe6f66049b781e2efa347463c52e4a269f0 eliminated pointless jedit_text_overview_limit; diff -r 42419fe6f660 -r 67c20ce71d22 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Sep 19 20:38:28 2015 +0200 +++ b/src/Tools/jEdit/etc/options Sat Sep 19 20:47:11 2015 +0200 @@ -30,9 +30,6 @@ public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" -public option jedit_text_overview_limit : int = 65536 - -- "maximum amount of text to visualize in overview column" - public option jedit_structure_limit : int = 1000 -- "maximum number of lines to scan for language structure" diff -r 42419fe6f660 -r 67c20ce71d22 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Sep 19 20:38:28 2015 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sat Sep 19 20:47:11 2015 +0200 @@ -360,8 +360,6 @@ /* command status overview */ - def overview_limit: Int = options.int("jedit_text_overview_limit") - def overview_color(range: Text.Range): Option[Color] = { if (snapshot.is_outdated) None diff -r 42419fe6f660 -r 67c20ce71d22 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Sat Sep 19 20:38:28 2015 +0200 +++ b/src/Tools/jEdit/src/text_overview.scala Sat Sep 19 20:47:11 2015 +0200 @@ -55,33 +55,17 @@ /* overview */ 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 def get_overview(rendering: Rendering): Overview = - { - val char_count = buffer.getLength + private def get_overview(): Overview = 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, + char_count = buffer.getLength, L = lines(), H = getHeight()) - } /* synchronous painting */ @@ -101,7 +85,7 @@ val rendering = doc_view.get_rendering() val snapshot = rendering.snapshot val options = rendering.options - val overview = get_overview(rendering) + val overview = get_overview() if (!snapshot.is_outdated && overview == current_overview) { gfx.setColor(getBackground) @@ -136,7 +120,7 @@ val rendering = doc_view.get_rendering() val snapshot = rendering.snapshot val options = rendering.options - val overview = get_overview(rendering) + val overview = get_overview() if (!snapshot.is_outdated && (overview != current_overview || @@ -155,7 +139,6 @@ 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 @@ -177,13 +160,9 @@ 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 { + (rendering.overview_color(Text.Range(start, end)), 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