tuned;
authorwenzelm
Mon, 14 Apr 2014 09:28:42 +0200
changeset 56569 1f9d706968c2
parent 56568 6e4f2d4215b0
child 56570 282f3b06fa86
tuned;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/spell_checker.scala
--- 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) =>