# HG changeset patch # User wenzelm # Date 1397331518 -7200 # Node ID 76cf86240cb74f52e60f73bdfb6394b497babaad # Parent d4da2b11c7293cd1716fbc48434a4bb27b10921f some case-mangling; clarified use of locale; diff -r d4da2b11c729 -r 76cf86240cb7 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Apr 12 21:00:04 2014 +0200 +++ b/src/Pure/System/options.scala Sat Apr 12 21:38:38 2014 +0200 @@ -58,7 +58,7 @@ case word :: rest if word == strip => rest case _ => words } - words1.map(Library.capitalize).mkString(" ") + words1.map(Library.capitalize(_)).mkString(" ") } def unknown: Boolean = typ == Unknown diff -r d4da2b11c729 -r 76cf86240cb7 src/Pure/library.scala --- a/src/Pure/library.scala Sat Apr 12 21:00:04 2014 +0200 +++ b/src/Pure/library.scala Sat Apr 12 21:38:38 2014 +0200 @@ -103,12 +103,19 @@ /* strings */ - def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH) - def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH) + def lowercase(str: String, locale: Locale = Locale.ENGLISH): String = str.toLowerCase(locale) + def uppercase(str: String, locale: Locale = Locale.ENGLISH): String = str.toUpperCase(locale) + + def capitalize(str: String, locale: Locale = Locale.ENGLISH): String = + if (str.length == 0) str + else uppercase(str.substring(0, 1), locale) + str.substring(1) - def capitalize(str: String): String = - if (str.length == 0) str - else uppercase(str.substring(0, 1)) + str.substring(1) + def is_capitalized(str: String): Boolean = + str.length > 0 && + Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_)) + + def is_all_caps(str: String): Boolean = + str.length > 0 && str.forall(Character.isUpperCase(_)) def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None diff -r d4da2b11c729 -r 76cf86240cb7 src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Sat Apr 12 21:00:04 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Sat Apr 12 21:38:38 2014 +0200 @@ -74,13 +74,19 @@ m.invoke(dictionary, word) } - def check(word: String): Boolean = + def contains(word: String): Boolean = { val m = dictionary.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String]) m.setAccessible(true) m.invoke(dictionary, word).asInstanceOf[java.lang.Boolean].booleanValue } + def check(word: String): Boolean = + contains(word) || + Library.is_all_caps(word) && contains(Library.lowercase(word, locale)) || + Library.is_capitalized(word) && + (contains(Library.lowercase(word, locale)) || contains(Library.uppercase(word, locale))) + def complete(word: String): List[String] = { val m = dictionary.getClass.getSuperclass. diff -r d4da2b11c729 -r 76cf86240cb7 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 21:00:04 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 21:38:38 2014 +0200 @@ -85,7 +85,7 @@ } reactions += { case ValueChanged(`search`) => delay_search.invoke() } }, "Search Symbols") - pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") ) + pages.map(p => p.title = space_explode('_', p.title).map(Library.capitalize(_)).mkString(" ")) } set_content(group_tabs) }