src/Tools/jEdit/src/jedit_lib.scala
changeset 49843 afddf4e26fac
parent 49712 a1bd8fe5131b
child 49941 f2db0596bd61
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 22:53:20 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 23:38:48 2012 +0200
     1.3 @@ -109,13 +109,6 @@
     1.4      }
     1.5  
     1.6  
     1.7 -  /* proper line range */
     1.8 -
     1.9 -  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
    1.10 -  def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
    1.11 -    Text.Range(start, end min buffer.getLength)
    1.12 -
    1.13 -
    1.14    /* visible text range */
    1.15  
    1.16    def visible_range(text_area: TextArea): Option[Text.Range] =
    1.17 @@ -125,7 +118,8 @@
    1.18      if (n > 0) {
    1.19        val start = text_area.getScreenLineStartOffset(0)
    1.20        val raw_end = text_area.getScreenLineEndOffset(n - 1)
    1.21 -      Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
    1.22 +      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
    1.23 +      Some(Text.Range(start, end))
    1.24      }
    1.25      else None
    1.26    }
    1.27 @@ -154,7 +148,7 @@
    1.28  
    1.29    class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.30  
    1.31 -  // NB: jEdit already normalizes \r\n and \r to \n
    1.32 +  // NB: jEdit always normalizes \r\n and \r to \n
    1.33    // NB: last line lacks \n
    1.34    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.35    {
    1.36 @@ -165,7 +159,7 @@
    1.37      val end = buffer.getLength
    1.38      val stop = range.stop
    1.39      val (q, r) =
    1.40 -      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
    1.41 +      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
    1.42        else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    1.43          (text_area.offsetToXY(stop - 1), char_width(text_area))
    1.44        else (text_area.offsetToXY(stop), 0)