src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -181,4 +181,32 @@
         (rest, remove(i, count, string))
       }
   }
+
+
+  /* text length wrt. encoding */
+
+  trait Length
+  {
+    def apply(text: String): Int
+    def offset(text: String, i: Int): Option[Text.Offset]
+  }
+
+  object Length extends Length
+  {
+    def apply(text: String): Int = text.length
+    def offset(text: String, i: Int): Option[Text.Offset] =
+      if (0 <= i && i <= text.length) Some(i) else None
+
+    val encodings: List[(String, Length)] =
+      List(
+        "UTF-16" -> Length,
+        "UTF-8" -> UTF8.Length,
+        "codepoints" -> Codepoint.Length,
+        "symbols" -> Symbol.Length)
+
+    def encoding(name: String): Length =
+      encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
+        error("Bad text length encoding: " + quote(name) +
+          " (expected " + commas_quote(encodings.map(_._1)) + ")")
+  }
 }