# HG changeset patch
# User wenzelm
# Date 1670341487 -3600
# Node ID 71942a6af4eda03412cd55c2cad220811943e840
# Parent  e5bf43eda6edd2cd99ec3a190192c465daff45ac
tuned signature;

diff -r e5bf43eda6ed -r 71942a6af4ed src/Tools/jEdit/src/jedit_spell_checker.scala
--- 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()