--- a/src/Pure/General/codepoint.scala Wed Jun 10 19:59:12 2020 +0200
+++ b/src/Pure/General/codepoint.scala Thu Jun 11 14:13:04 2020 +0200
@@ -6,22 +6,29 @@
package isabelle
+import isabelle.Text.Offset
+
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
- }
+ private class Iterator_Offset[A](s: String, result: (Int, Text.Offset) => A)
+ extends Iterator[A]
+ {
+ var offset = 0
+ def hasNext: Boolean = offset < s.length
+ def next: A =
+ {
+ val c = s.codePointAt(offset)
+ val i = offset
+ offset += Character.charCount(c)
+ result(c, i)
}
+ }
+
+ def iterator_offset(s: String): Iterator[(Int, Text.Offset)] = new Iterator_Offset(s, (_, _))
+ def iterator(s: String): Iterator[Int] = new Iterator_Offset(s, (c, _) => c)
def length(s: String): Int = iterator(s).length
}