diff -r 88211daacf93 -r fd0d6de380c6 src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Tue Dec 20 10:06:18 2016 +0100
+++ b/src/Pure/General/codepoint.scala	Tue Dec 20 10:44:36 2016 +0100
@@ -9,17 +9,20 @@
 
 object Codepoint
 {
-  def iterator(str: String): Iterator[Int] =
+  def string(c: Int): String = new String(Array(c), 0, 1)
+
+  def iterator(s: String): Iterator[Int] =
     new Iterator[Int] {
       var offset = 0
-      def hasNext: Boolean = offset < str.length
+      def hasNext: Boolean = offset < s.length
       def next: Int =
       {
-        val c = str.codePointAt(offset)
+        val c = s.codePointAt(offset)
         offset += Character.charCount(c)
         c
       }
     }
 
-  def string(c: Int): String = new String(Array(c), 0, 1)
+  def length(s: String): Int = iterator(s).length
+  object Length extends Line.Length { def apply(s: String): Int = Codepoint.length(s) }
 }