--- a/src/Pure/General/word.scala Tue Aug 29 17:53:36 2023 +0200
+++ b/src/Pure/General/word.scala Tue Aug 29 18:13:30 2023 +0200
@@ -37,32 +37,29 @@
capitalize(str)
else str
- sealed abstract class Case
- case object Lowercase extends Case
- case object Uppercase extends Case
- case object Capitalized extends Case
-
object Case {
def apply(c: Case, str: String): String =
c match {
- case Lowercase => lowercase(str)
- case Uppercase => uppercase(str)
- case Capitalized => capitalize(str)
+ case Case.lowercase => Word.lowercase(str)
+ case Case.uppercase => Word.uppercase(str)
+ case Case.capitalized => Word.capitalize(str)
}
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(Case.lowercase)
+ else if (Codepoint.iterator(str).forall(Character.isUpperCase)) Some(Case.uppercase)
else {
val it = Codepoint.iterator(str)
if (Character.isUpperCase(it.next()) && it.forall(Character.isLowerCase))
- Some(Capitalized)
+ Some(Case.capitalized)
else None
}
}
else None
}
+ enum Case { case lowercase, uppercase, capitalized }
+
/* sequence of words */
--- a/src/Pure/Tools/spell_checker.scala Tue Aug 29 17:53:36 2023 +0200
+++ b/src/Pure/Tools/spell_checker.scala Tue Aug 29 18:13:30 2023 +0200
@@ -201,7 +201,7 @@
def check(word: String): Boolean =
word match {
- case Word.Case(c) if c != Word.Lowercase =>
+ case Word.Case(c) if c != Word.Case.lowercase =>
contains(word) || contains(Word.lowercase(word))
case _ =>
contains(word)
@@ -231,7 +231,7 @@
}
val result =
word_case match {
- case Some(c) if c != Word.Lowercase =>
+ case Some(c) if c != Word.Case.lowercase =>
suggestions(word) orElse suggestions(Word.lowercase(word))
case _ =>
suggestions(word)