src/Pure/PIDE/text.scala
changeset 65155 25bccf5bf33e
parent 65154 ba1929b749f0
child 65156 35fefc249311
     1.1 --- a/src/Pure/PIDE/text.scala	Wed Mar 08 20:25:57 2017 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Mar 08 20:30:05 2017 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5      override def toString: String = "[" + start.toString + ".." + stop.toString + "]"
     1.6  
     1.7 -    def length: Int = stop - start
     1.8 +    def length: Offset = stop - start
     1.9  
    1.10      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    1.11      def +(i: Offset): Range = if (i == 0) this else map(_ + i)
    1.12 @@ -169,13 +169,13 @@
    1.13      private def insert(i: Offset, string: String): String =
    1.14        string.substring(0, i) + text + string.substring(i)
    1.15  
    1.16 -    private def remove(i: Offset, count: Int, string: String): String =
    1.17 +    private def remove(i: Offset, count: Offset, string: String): String =
    1.18        string.substring(0, i) + string.substring(i + count)
    1.19  
    1.20 -    def can_edit(string: String, shift: Int): Boolean =
    1.21 +    def can_edit(string: String, shift: Offset): Boolean =
    1.22        shift <= start && start < shift + string.length
    1.23  
    1.24 -    def edit(string: String, shift: Int): (Option[Edit], String) =
    1.25 +    def edit(string: String, shift: Offset): (Option[Edit], String) =
    1.26        if (!can_edit(string, shift)) (Some(this), string)
    1.27        else if (is_insert) (None, insert(start - shift, string))
    1.28        else {