src/Tools/jEdit/src/jedit_lib.scala
changeset 56589 71c5d1f516c0
parent 56587 83777a91f5de
child 56592 5157f7615e99
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 12:45:16 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 13:07:59 2014 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4      Text.Range(0, buffer.getLength)
     1.5  
     1.6    def line_range(buffer: JEditBuffer, line: Int): Text.Range =
     1.7 -    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))
     1.8 +    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
     1.9  
    1.10    def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
    1.11    {