--- a/src/Tools/jEdit/src/document_model.scala Mon Sep 17 17:49:11 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Sep 17 17:56:10 2012 +0200
@@ -92,24 +92,6 @@
}
-
- /* point range */
-
- def point_range(offset: Text.Offset): Text.Range =
- JEdit_Lib.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