src/Pure/General/word.scala
changeset 56601 8f80a243857d
parent 56600 628e039cc34d
child 56602 e7e20d72756a
equal deleted inserted replaced
56600:628e039cc34d 56601:8f80a243857d
    11 import java.util.Locale
    11 import java.util.Locale
    12 
    12 
    13 
    13 
    14 object Word
    14 object Word
    15 {
    15 {
       
    16   /* codepoints */
       
    17 
       
    18   def codepoint_iterator(str: String): Iterator[Int] =
       
    19     new Iterator[Int] {
       
    20       var offset = 0
       
    21       def hasNext: Boolean = offset < str.length
       
    22       def next: Int =
       
    23       {
       
    24         val c = str.codePointAt(offset)
       
    25         offset += Character.charCount(c)
       
    26         c
       
    27       }
       
    28     }
       
    29 
       
    30 
    16   /* case */
    31   /* case */
    17 
    32 
    18   def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
    33   def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
    19   def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
    34   def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
    20 
    35 
    21   def capitalize(str: String): String =
    36   def capitalize(str: String): String =
    22     if (str.length == 0) str
    37     if (str.length == 0) str
    23     else uppercase(str.substring(0, 1)) + str.substring(1)
    38     else {
       
    39       val n = Character.charCount(str.codePointAt(0))
       
    40       uppercase(str.substring(0, n)) + str.substring(n)
       
    41     }
       
    42 
       
    43   sealed abstract class Case
       
    44   case object Lowercase extends Case
       
    45   case object Uppercase extends Case
       
    46   case object Capitalized extends Case
       
    47 
       
    48   object Case
       
    49   {
       
    50     def apply(c: Case, str: String): String =
       
    51       c match {
       
    52         case Lowercase => lowercase(str)
       
    53         case Uppercase => uppercase(str)
       
    54         case Capitalized => capitalize(str)
       
    55       }
       
    56     def unapply(str: String): Option[Case] =
       
    57       if (!str.isEmpty) {
       
    58         if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
       
    59         else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
       
    60         else {
       
    61           val it = codepoint_iterator(str)
       
    62           if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
       
    63             Some(Capitalized)
       
    64           else None
       
    65         }
       
    66       }
       
    67       else None
       
    68   }
    24 
    69 
    25   def is_capitalized(str: String): Boolean =
    70   def is_capitalized(str: String): Boolean =
    26     str.length > 0 &&
    71     str.length > 0 &&
    27     Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_))
    72     Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_))
    28 
    73