# HG changeset patch
# User wenzelm
# Date 1358171182 -3600
# Node ID 05054cf8ca77fea95ca39f31b76af4b933b68217
# Parent  f3588e59aeaa64b454be4d2e2f3bc4e8fe3c905a
more precise relevant_range to exploit overview_limit better;

diff -r f3588e59aeaa -r 05054cf8ca77 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 13:59:43 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 14:46:22 2013 +0100
@@ -91,9 +91,12 @@
               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) max 0
-                val stop = (start + len) min char_count
-                Text.Range(start, stop)
+                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 &&