| author | wenzelm |
| Tue, 20 Dec 2016 08:53:26 +0100 | |
| changeset 64610 | 1b89608974e9 |
| child 64615 | fd0d6de380c6 |
| permissions | -rw-r--r-- |
| 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 |
{
|
|
12 |
def iterator(str: String): Iterator[Int] = |
|
13 |
new Iterator[Int] {
|
|
14 |
var offset = 0 |
|
15 |
def hasNext: Boolean = offset < str.length |
|
16 |
def next: Int = |
|
17 |
{
|
|
18 |
val c = str.codePointAt(offset) |
|
19 |
offset += Character.charCount(c) |
|
20 |
c |
|
21 |
} |
|
22 |
} |
|
23 |
||
24 |
def string(c: Int): String = new String(Array(c), 0, 1) |
|
25 |
} |