clarified signature: prefer enum types;
authorwenzelm
Tue, 29 Aug 2023 18:13:30 +0200
changeset 78613 60561d28569b
parent 78612 f7df1a444dbb
child 78614 4da5cdaa4dcd
clarified signature: prefer enum types;
src/Pure/General/word.scala
src/Pure/Tools/spell_checker.scala
--- 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)