src/Tools/jEdit/src/document_view.scala
changeset 43448 90aec5043461
parent 43419 6ed49c52d463
child 43510 17d431c92575
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Jun 18 18:57:38 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Jun 18 21:03:52 2011 +0200
     1.3 @@ -302,6 +302,24 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* caret range */
     1.8 +
     1.9 +  def caret_range(): Text.Range =
    1.10 +    Isabelle.buffer_lock(model.buffer) {
    1.11 +      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
    1.12 +      val caret = text_area.getCaretPosition
    1.13 +      try {
    1.14 +        val c = text(caret)
    1.15 +        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
    1.16 +          Text.Range(caret, caret + 2)
    1.17 +        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
    1.18 +          Text.Range(caret - 1, caret + 1)
    1.19 +        else Text.Range(caret, caret + 1)
    1.20 +      }
    1.21 +      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
    1.22 +    }
    1.23 +
    1.24 +
    1.25    /* caret handling */
    1.26  
    1.27    def selected_command(): Option[Command] =