# HG changeset patch
# User wenzelm
# Date 1660384425 -7200
# Node ID 93a704c52061b9b91aa7673d80e0aa4fc88ec82b
# Parent  0855dc42b53537d5ae1545b587d49de9d8d54964
tuned, following 298707451ec2;
tuned signature;

diff -r 0855dc42b535 -r 93a704c52061 src/Tools/jEdit/src/jedit_sessions.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"
diff -r 0855dc42b535 -r 93a704c52061 src/Tools/jEdit/src/jedit_spell_checker.scala
--- 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
   }
 }