src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -190,32 +190,4 @@
         (rest, remove(i, count, string))
       }
   }
-
-
-  /* text length wrt. encoding */
-
-  trait Length
-  {
-    def apply(text: String): Int
-    def offset(text: String, i: Int): Option[Offset]
-  }
-
-  object Length extends Length
-  {
-    def apply(text: String): Int = text.length
-    def offset(text: String, i: Int): Option[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)) + ")")
-  }
 }