src/Pure/General/codepoint.scala
author wenzelm
Tue, 20 Dec 2016 08:53:26 +0100
changeset 64610 1b89608974e9
child 64615 fd0d6de380c6
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64610
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/codepoint.scala
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     3
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     4
Unicode codepoints vs. Unicode string encoding.
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     6
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     8
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
     9
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    10
object Codepoint
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    11
{
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    12
  def iterator(str: String): Iterator[Int] =
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    13
    new Iterator[Int] {
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    14
      var offset = 0
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    15
      def hasNext: Boolean = offset < str.length
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    16
      def next: Int =
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    17
      {
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    18
        val c = str.codePointAt(offset)
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    19
        offset += Character.charCount(c)
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    20
        c
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    21
      }
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    22
    }
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    23
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    24
  def string(c: Int): String = new String(Array(c), 0, 1)
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    25
}