# HG changeset patch
# User wenzelm
# Date 1489001405 -3600
# Node ID 25bccf5bf33e4bbd1ebac963d6155edb75e10eaf
# Parent  ba1929b749f049a1418a206bc7f805dbe7b74fbc
clarified native Text.Offset versus Text.Length index Int;

diff -r ba1929b749f0 -r 25bccf5bf33e src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Mar 08 20:25:57 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Mar 08 20:30:05 2017 +0100
@@ -42,7 +42,7 @@
 
     override def toString: String = "[" + start.toString + ".." + stop.toString + "]"
 
-    def length: Int = stop - start
+    def length: Offset = stop - start
 
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = if (i == 0) this else map(_ + i)
@@ -169,13 +169,13 @@
     private def insert(i: Offset, string: String): String =
       string.substring(0, i) + text + string.substring(i)
 
-    private def remove(i: Offset, count: Int, string: String): String =
+    private def remove(i: Offset, count: Offset, string: String): String =
       string.substring(0, i) + string.substring(i + count)
 
-    def can_edit(string: String, shift: Int): Boolean =
+    def can_edit(string: String, shift: Offset): Boolean =
       shift <= start && start < shift + string.length
 
-    def edit(string: String, shift: Int): (Option[Edit], String) =
+    def edit(string: String, shift: Offset): (Option[Edit], String) =
       if (!can_edit(string, shift)) (Some(this), string)
       else if (is_insert) (None, insert(start - shift, string))
       else {