src/Pure/General/word.scala
changeset 57087 16536c15d749
parent 56792 792dd0e9cebb
child 59319 677615cba30d
equal deleted inserted replaced
57086:db7c735e963d 57087:16536c15d749
    41       val n = Character.charCount(str.codePointAt(0))
    41       val n = Character.charCount(str.codePointAt(0))
    42       uppercase(str.substring(0, n)) + lowercase(str.substring(n))
    42       uppercase(str.substring(0, n)) + lowercase(str.substring(n))
    43     }
    43     }
    44 
    44 
    45   def perhaps_capitalize(str: String): String =
    45   def perhaps_capitalize(str: String): String =
    46     str match {
    46     if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
    47       case Case(c) if c != Lowercase => str
    47       capitalize(str)
    48       case _ => capitalize(str)
    48     else str
    49     }
       
    50 
    49 
    51   sealed abstract class Case
    50   sealed abstract class Case
    52   case object Lowercase extends Case
    51   case object Lowercase extends Case
    53   case object Uppercase extends Case
    52   case object Uppercase extends Case
    54   case object Capitalized extends Case
    53   case object Capitalized extends Case