src/Tools/jEdit/src/jedit_lib.scala
changeset 56592 5157f7615e99
parent 56589 71c5d1f516c0
child 56593 0ea7c84110ac
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:11:34 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:27:50 2014 +0200
     1.3 @@ -162,19 +162,21 @@
     1.4    /* point range */
     1.5  
     1.6    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     1.7 -    buffer_lock(buffer) {
     1.8 -      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
     1.9 -      try {
    1.10 -        val c = text(offset)
    1.11 -        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    1.12 -          Text.Range(offset, offset + 2)
    1.13 -        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    1.14 -          Text.Range(offset - 1, offset + 1)
    1.15 -        else
    1.16 -          Text.Range(offset, offset + 1)
    1.17 +    if (offset < 0) Text.Range.offside
    1.18 +    else
    1.19 +      buffer_lock(buffer) {
    1.20 +        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
    1.21 +        try {
    1.22 +          val c = text(offset)
    1.23 +          if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    1.24 +            Text.Range(offset, offset + 2)
    1.25 +          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    1.26 +            Text.Range(offset - 1, offset + 1)
    1.27 +          else
    1.28 +            Text.Range(offset, offset + 1)
    1.29 +        }
    1.30 +        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    1.31        }
    1.32 -      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    1.33 -    }
    1.34  
    1.35  
    1.36    /* text ranges */
    1.37 @@ -185,6 +187,9 @@
    1.38    def line_range(buffer: JEditBuffer, line: Int): Text.Range =
    1.39      Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
    1.40  
    1.41 +  def caret_range(text_area: TextArea): Text.Range =
    1.42 +    point_range(text_area.getBuffer, text_area.getCaretPosition)
    1.43 +
    1.44    def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
    1.45    {
    1.46      val range = line_range(text_area.getBuffer, text_area.getCaretLine)