1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 19:17:39 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 19:55:31 2012 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
     1.5  import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
     1.6  import javax.swing.event.{CaretListener, CaretEvent}
     1.7 -import javax.swing.text.Segment
     1.8  
     1.9  import org.gjt.sp.util.Log
    1.10  
    1.11 @@ -317,18 +316,19 @@
    1.12    /* caret range */
    1.13  
    1.14    def caret_range(): Text.Range =
    1.15 -  {
    1.16 -    val buffer = model.buffer
    1.17 -    Isabelle.buffer_lock(buffer) {
    1.18 -      val max = buffer.getLength
    1.19 -      val text = new Segment; buffer.getText(0, max, text)
    1.20 -      val chars = BreakIterator.getCharacterInstance(); chars.setText(text)
    1.21 -
    1.22 -      val stop = chars.following(text_area.getCaretPosition)
    1.23 -      if (stop < 0) Text.Range(max, max)
    1.24 -      else Text.Range(chars.previous(), stop)
    1.25 +    Isabelle.buffer_lock(model.buffer) {
    1.26 +      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
    1.27 +      val caret = text_area.getCaretPosition
    1.28 +      try {
    1.29 +        val c = text(caret)
    1.30 +        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
    1.31 +          Text.Range(caret, caret + 2)
    1.32 +        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
    1.33 +          Text.Range(caret - 1, caret + 1)
    1.34 +        else Text.Range(caret, caret + 1)
    1.35 +      }
    1.36 +      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
    1.37      }
    1.38 -  }
    1.39  
    1.40  
    1.41    /* caret handling */