tuned, following 298707451ec2;
authorwenzelm
Sat, 13 Aug 2022 11:53:45 +0200
changeset 75837 93a704c52061
parent 75836 0855dc42b535
child 75838 7f6803788de3
tuned, following 298707451ec2; tuned signature;
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sat Aug 13 11:36:24 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sat Aug 13 11:53:45 2022 +0200
@@ -90,7 +90,7 @@
 
     val entries = default_entry :: session_entries
 
-    new ComboBox(entries) with Option_Component {
+    new ComboBox[Logic_Entry](entries) with Option_Component {
       name = jedit_logic_option
       tooltip = "Logic session name (change requires restart)"
       val title = "Logic"
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Sat Aug 13 11:36:24 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Sat Aug 13 11:53:45 2022 +0200
@@ -87,8 +87,10 @@
     val opt = PIDE.options.value.check_name(option_name)
 
     val entries = Spell_Checker.dictionaries
-    val component = new ComboBox(entries) with Option_Component {
+
+    new ComboBox[Spell_Checker.Dictionary](entries) with Option_Component {
       name = option_name
+      tooltip = GUI.tooltip_lines(opt.print_default)
       val title = opt.title()
       def load(): Unit = {
         val lang = PIDE.options.string(option_name)
@@ -98,10 +100,8 @@
         }
       }
       def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
+
+      load()
     }
-
-    component.load()
-    component.tooltip = GUI.tooltip_lines(opt.print_default)
-    component
   }
 }