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