--- a/src/Pure/General/word.scala Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/General/word.scala Tue Dec 20 08:53:26 2016 +0100
@@ -12,23 +12,6 @@
object Word
{
- /* codepoints */
-
- def codepoint_iterator(str: String): Iterator[Int] =
- new Iterator[Int] {
- var offset = 0
- def hasNext: Boolean = offset < str.length
- def next: Int =
- {
- val c = str.codePointAt(offset)
- offset += Character.charCount(c)
- c
- }
- }
-
- def codepoint(c: Int): String = new String(Array(c), 0, 1)
-
-
/* directionality */
def bidi_detect(str: String): Boolean =
@@ -51,7 +34,7 @@
}
def perhaps_capitalize(str: String): String =
- if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
+ if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
capitalize(str)
else str
@@ -70,10 +53,10 @@
}
def unapply(str: String): Option[Case] =
if (str.nonEmpty) {
- if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
- else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
+ if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
+ else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
else {
- val it = codepoint_iterator(str)
+ val it = Codepoint.iterator(str)
if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
Some(Capitalized)
else None