src/Pure/General/utf8.scala
changeset 65196 e8760a98db78
parent 64639 bad5de3f9554
child 68224 1f7308050349
--- a/src/Pure/General/utf8.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/General/utf8.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -21,15 +21,6 @@
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
-  object Length extends Codepoint.Length
-  {
-    override def codepoint_length(c: Int): Int =
-      if (c < 0x80) 1
-      else if (c < 0x800) 2
-      else if (c < 0x10000) 3
-      else 4
-  }
-
 
   /* permissive UTF-8 decoding */