--- 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
}
}