--- a/src/Pure/PIDE/text.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Pure/PIDE/text.scala Sun Aug 15 22:48:56 2010 +0200
@@ -10,15 +10,22 @@
object Text
{
- /* edits */
+ /* offset and range */
+
+ type Offset = Int
+
+ sealed case class Range(val start: Offset, val stop: Offset)
+
+
+ /* editing */
object Edit
{
- def insert(start: Int, text: String): Edit = new Edit(true, start, text)
- def remove(start: Int, text: String): Edit = new Edit(false, start, text)
+ def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
+ def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
}
- class Edit(val is_insert: Boolean, val start: Int, val text: String)
+ class Edit(val is_insert: Boolean, val start: Offset, val text: String)
{
override def toString =
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
@@ -26,22 +33,22 @@
/* transform offsets */
- private def transform(do_insert: Boolean, offset: Int): Int =
- if (offset < start) offset
- else if (is_insert == do_insert) offset + text.length
- else (offset - text.length) max start
+ private def transform(do_insert: Boolean, i: Offset): Offset =
+ if (i < start) i
+ else if (is_insert == do_insert) i + text.length
+ else (i - text.length) max start
- def convert(offset: Int): Int = transform(true, offset)
- def revert(offset: Int): Int = transform(false, offset)
+ def convert(i: Offset): Offset = transform(true, i)
+ def revert(i: Offset): Offset = transform(false, i)
/* edit strings */
- private def insert(index: Int, string: String): String =
- string.substring(0, index) + text + string.substring(index)
+ private def insert(i: Offset, string: String): String =
+ string.substring(0, i) + text + string.substring(i)
- private def remove(index: Int, count: Int, string: String): String =
- string.substring(0, index) + string.substring(index + count)
+ private def remove(i: Offset, count: Int, string: String): String =
+ string.substring(0, i) + string.substring(i + count)
def can_edit(string: String, shift: Int): Boolean =
shift <= start && start < shift + string.length
@@ -50,12 +57,12 @@
if (!can_edit(string, shift)) (Some(this), string)
else if (is_insert) (None, insert(start - shift, string))
else {
- val index = start - shift
- val count = text.length min (string.length - index)
+ val i = start - shift
+ val count = text.length min (string.length - i)
val rest =
if (count == text.length) None
else Some(Edit.remove(start, text.substring(count)))
- (rest, remove(index, count, string))
+ (rest, remove(i, count, string))
}
}
}