src/Pure/General/codepoint.scala
author wenzelm
Wed, 20 Mar 2019 23:06:51 +0100
changeset 69933 c15ee153dec1
parent 65196 e8760a98db78
child 71933 aec0f7b58cc6
permissions -rw-r--r--
updated to cygwin-20190320;
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
{
64615
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    12
  def string(c: Int): String = new String(Array(c), 0, 1)
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    13
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    14
  def iterator(s: String): Iterator[Int] =
64610
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    15
    new Iterator[Int] {
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    16
      var offset = 0
64615
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    17
      def hasNext: Boolean = offset < s.length
64610
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    18
      def next: Int =
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    19
      {
64615
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    20
        val c = s.codePointAt(offset)
64610
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    21
        offset += Character.charCount(c)
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    22
        c
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    23
      }
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    24
    }
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    25
64615
fd0d6de380c6 more systematic text length;
wenzelm
parents: 64610
diff changeset
    26
  def length(s: String): Int = iterator(s).length
64610
1b89608974e9 clarified modules;
wenzelm
parents:
diff changeset
    27
}