1/* Title: Pure/General/codepoint.scala 2 Author: Makarius 3 4Unicode codepoints vs. Unicode string encoding. 5*/ 6 7package isabelle 8 9 10object Codepoint 11{ 12 def string(c: Int): String = new String(Array(c), 0, 1) 13 14 def iterator(s: String): Iterator[Int] = 15 new Iterator[Int] { 16 var offset = 0 17 def hasNext: Boolean = offset < s.length 18 def next: Int = 19 { 20 val c = s.codePointAt(offset) 21 offset += Character.charCount(c) 22 c 23 } 24 } 25 26 def length(s: String): Int = iterator(s).length 27} 28