eliminated somewhat pointless locale parameter;
authorwenzelm
Mon, 14 Apr 2014 09:24:47 +0200
changeset 56568 6e4f2d4215b0
parent 56567 7adad03f2cef
child 56569 1f9d706968c2
eliminated somewhat pointless locale parameter;
src/Pure/library.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/spell_checker.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 &&
--- 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"
--- 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