diff -r ffab6f460a82 -r e8760a98db78 src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/General/codepoint.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -24,30 +24,4 @@
     }
 
   def length(s: String): Int = iterator(s).length
-
-  trait Length extends Text.Length
-  {
-    protected def codepoint_length(c: Int): Int = 1
-
-    def apply(s: String): Int =
-      (0 /: iterator(s)) { case (n, c) => n + codepoint_length(c) }
-
-    def offset(s: String, i: Int): Option[Text.Offset] =
-    {
-      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
-      else {
-        val length = s.length
-        var offset = 0
-        var j = 0
-        while (offset < length && j < i) {
-          val c = s.codePointAt(offset)
-          offset += Character.charCount(c)
-          j += codepoint_length(c)
-        }
-        if (j >= i) Some(offset) else None
-      }
-    }
-  }
-
-  object Length extends Length
 }