| author | wenzelm | 
| Tue, 20 Dec 2016 08:53:26 +0100 | |
| changeset 64610 | 1b89608974e9 | 
| child 64615 | fd0d6de380c6 | 
| permissions | -rw-r--r-- | 
/* 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) }