| 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 | }
 |