--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 14 13:52:16 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 14 17:37:19 2012 +0200
@@ -92,6 +92,24 @@
}
+
+ /* point range */
+
+ def point_range(offset: Text.Offset): Text.Range =
+ Isabelle.buffer_lock(buffer) {
+ def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
+ try {
+ val c = text(offset)
+ if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
+ Text.Range(offset, offset + 2)
+ else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
+ Text.Range(offset - 1, offset + 1)
+ else Text.Range(offset, offset + 1)
+ }
+ catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
+ }
+
+
/* pending text edits */
private object pending_edits // owned by Swing thread