--- a/src/Tools/jEdit/etc/options Mon Apr 14 09:24:47 2014 +0200
+++ b/src/Tools/jEdit/etc/options Mon Apr 14 09:28:42 2014 +0200
@@ -54,7 +54,7 @@
public option spell_checker : bool = true
-- "enable spell-checker for prose words within document text, comments etc."
-public option spell_checker_language : string = "en_US"
+public option spell_checker_dictionary : string = "en_US"
-- "spell-checker dictionary name"
public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
--- a/src/Tools/jEdit/src/spell_checker.scala Mon Apr 14 09:24:47 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Mon Apr 14 09:28:42 2014 +0200
@@ -83,7 +83,7 @@
{
Swing_Thread.require()
- val option_name = "spell_checker_language"
+ val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
val entries = dictionaries()
@@ -175,7 +175,7 @@
def update(options: Options): Unit = synchronized {
if (options.bool("spell_checker")) {
- val lang = options.string("spell_checker_language")
+ val lang = options.string("spell_checker_dictionary")
if (current_spell_checker._1 != lang) {
Spell_Checker.dictionaries.find(_.lang == lang) match {
case Some(dictionary) =>