src/Pure/General/codepoint.scala
author wenzelm
Fri, 17 Mar 2017 20:33:27 +0100
changeset 65292 e3bd1e7ddd23
parent 65196 e8760a98db78
child 71933 aec0f7b58cc6
permissions -rw-r--r--
more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;

/*  Title:      Pure/General/codepoint.scala
    Author:     Makarius

Unicode codepoints vs. Unicode string encoding.
*/

package isabelle


object Codepoint
{
  def string(c: Int): String = new String(Array(c), 0, 1)

  def iterator(s: String): Iterator[Int] =
    new Iterator[Int] {
      var offset = 0
      def hasNext: Boolean = offset < s.length
      def next: Int =
      {
        val c = s.codePointAt(offset)
        offset += Character.charCount(c)
        c
      }
    }

  def length(s: String): Int = iterator(s).length
}