some case-mangling;
clarified use of locale;

--- 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

--- 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

--- 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.

--- 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)
 }