# HG changeset patch
# User wenzelm
# Date 1397460287 -7200
# Node ID 6e4f2d4215b019567f118e049f1d531c6d1534c9
# Parent  7adad03f2cefccaa5f6f9b27434c497aa791fc14
eliminated somewhat pointless locale parameter;

diff -r 7adad03f2cef -r 6e4f2d4215b0 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Apr 13 22:08:00 2014 +0200
+++ b/src/Pure/library.scala	Mon Apr 14 09:24:47 2014 +0200
@@ -103,12 +103,12 @@
 
   /* strings */
 
-  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 lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
+  def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
 
-  def capitalize(str: String, locale: Locale = Locale.ENGLISH): String =
+  def capitalize(str: String): String =
     if (str.length == 0) str
-    else uppercase(str.substring(0, 1), locale) + str.substring(1)
+    else uppercase(str.substring(0, 1)) + str.substring(1)
 
   def is_capitalized(str: String): Boolean =
     str.length > 0 &&
diff -r 7adad03f2cef -r 6e4f2d4215b0 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sun Apr 13 22:08:00 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Apr 14 09:24:47 2014 +0200
@@ -55,7 +55,7 @@
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_language : string = "en_US"
-  -- "language for spell-checker locale and dictionary"
+  -- "spell-checker dictionary name"
 
 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
   -- "relevant markup elements for spell-checker, separated by commas"
diff -r 7adad03f2cef -r 6e4f2d4215b0 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 22:08:00 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 09:24:47 2014 +0200
@@ -11,7 +11,6 @@
 import isabelle._
 
 import java.lang.Class
-import java.util.Locale
 
 import scala.collection.mutable
 import scala.swing.ComboBox
@@ -63,12 +62,6 @@
     val lang = path.split_ext._1.base.implode
     override def toString: String = lang
 
-    val locale: Locale =
-      space_explode('_', lang) match {
-        case l :: _ => Locale.forLanguageTag(l)
-        case Nil => Locale.ENGLISH
-      }
-
     def load_words: List[String] =
       path.split_ext._2 match {
         case "gz" => split_lines(File.read_gzip(path))
@@ -156,10 +149,9 @@
 
   def check(word: String): Boolean =
     contains(word) ||
-    Library.is_all_caps(word) && contains(Library.lowercase(word, dictionary.locale)) ||
+    Library.is_all_caps(word) && contains(Library.lowercase(word)) ||
     Library.is_capitalized(word) &&
-      (contains(Library.lowercase(word, dictionary.locale)) ||
-       contains(Library.uppercase(word, dictionary.locale)))
+      (contains(Library.lowercase(word)) || contains(Library.uppercase(word)))
 
   def complete(word: String): List[String] =
     if (check(word)) Nil