# HG changeset patch
# User wenzelm
# Date 1322914310 -3600
# Node ID 0ad063afa3d64f5d15682c0c7a0fed6c39d9da2d
# Parent  857b7fcb03653874e49edcd8c7c7887821f22a48
caret_range based on BreakIterator, which handles combined unicode characters as well;

diff -r 857b7fcb0365 -r 0ad063afa3d6 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Dec 02 16:37:35 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Dec 03 13:11:50 2011 +0100
@@ -15,11 +15,13 @@
 import scala.actors.Actor._
 
 import java.lang.System
+import java.text.BreakIterator
 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
   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
 
@@ -348,19 +350,18 @@
   /* caret range */
 
   def caret_range(): Text.Range =
-    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) }
+  {
+    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)
     }
+  }
 
 
   /* caret handling */