diff -r 302d3ecff25d -r d8286601e7df src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 19:17:39 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Jan 15 19:55:31 2012 +0100
@@ -21,7 +21,6 @@
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
 import javax.swing.event.{CaretListener, CaretEvent}
-import javax.swing.text.Segment
 
 import org.gjt.sp.util.Log
 
@@ -317,18 +316,19 @@
   /* caret range */
 
   def caret_range(): Text.Range =
-  {
-    val buffer = model.buffer
-    Isabelle.buffer_lock(buffer) {
-      val max = buffer.getLength
-      val text = new Segment; buffer.getText(0, max, text)
-      val chars = BreakIterator.getCharacterInstance(); chars.setText(text)
-
-      val stop = chars.following(text_area.getCaretPosition)
-      if (stop < 0) Text.Range(max, max)
-      else Text.Range(chars.previous(), stop)
+    Isabelle.buffer_lock(model.buffer) {
+      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
+      val caret = text_area.getCaretPosition
+      try {
+        val c = text(caret)
+        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
+          Text.Range(caret, caret + 2)
+        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
+          Text.Range(caret - 1, caret + 1)
+        else Text.Range(caret, caret + 1)
+      }
+      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
     }
-  }
 
 
   /* caret handling */