diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/General/codepoint.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/codepoint.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -0,0 +1,25 @@
+/*  Title:      Pure/General/codepoint.scala
+    Author:     Makarius
+
+Unicode codepoints vs. Unicode string encoding.
+*/
+
+package isabelle
+
+
+object Codepoint
+{
+  def iterator(str: String): Iterator[Int] =
+    new Iterator[Int] {
+      var offset = 0
+      def hasNext: Boolean = offset < str.length
+      def next: Int =
+      {
+        val c = str.codePointAt(offset)
+        offset += Character.charCount(c)
+        c
+      }
+    }
+
+  def string(c: Int): String = new String(Array(c), 0, 1)
+}