changeset 59319 | 677615cba30d |
parent 57087 | 16536c15d749 |
child 62812 | ce22e5c3d4ce |
--- a/src/Pure/General/word.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/word.scala Thu Jan 08 20:56:39 2015 +0100 @@ -61,7 +61,7 @@ case Capitalized => capitalize(str) } def unapply(str: String): Option[Case] = - if (!str.isEmpty) { + if (str.nonEmpty) { if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) else {