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