| author | blanchet | 
| Tue, 19 Dec 2017 14:51:27 +0100 | |
| changeset 67225 | cb34f5f49a08 | 
| parent 65196 | e8760a98db78 | 
| child 71933 | aec0f7b58cc6 | 
| permissions | -rw-r--r-- | 
/* Title: Pure/General/codepoint.scala Author: Makarius Unicode codepoints vs. Unicode string encoding. */ package isabelle object Codepoint { 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 < s.length def next: Int = { val c = s.codePointAt(offset) offset += Character.charCount(c) c } } def length(s: String): Int = iterator(s).length }