src/Pure/General/codepoint.scala

--- a/src/Pure/General/codepoint.scala	Tue Dec 20 10:45:20 2016 +0100
+++ b/src/Pure/General/codepoint.scala	Tue Dec 20 16:08:02 2016 +0100
@@ -24,5 +24,30 @@
     }
 
   def length(s: String): Int = iterator(s).length
-  object Length extends Line.Length { def apply(s: String): Int = Codepoint.length(s) }
+
+  trait Length extends isabelle.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)) isabelle.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
 }