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