tuned signature;

--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Dec 06 16:42:08 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Dec 06 16:44:47 2022 +0100
@@ -88,15 +88,16 @@
     new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.item)) with JEdit_Options.Entry {
       name = option_name
       tooltip = GUI.tooltip_lines(opt.print_default)
-      val title = opt.title()
-      def load(): Unit = {
+
+      override val title: String = opt.title_jedit
+      override def load(): Unit = {
         val lang = PIDE.options.string(option_name)
         Spell_Checker.get_dictionary(lang) match {
           case Some(dict) => selection.item = GUI.Selector.item(dict)
           case None =>
         }
       }
-      def save(): Unit =
+      override def save(): Unit =
         for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang
 
       load()