--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Aug 13 11:59:06 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Aug 13 12:32:38 2022 +0200
@@ -10,7 +10,6 @@
import isabelle._
import javax.swing.JMenuItem
-import scala.swing.ComboBox
import org.gjt.sp.jedit.menu.EnhancedMenuItem
import org.gjt.sp.jedit.jEdit
@@ -86,9 +85,7 @@
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
- val entries = Spell_Checker.dictionaries
-
- new ComboBox[Spell_Checker.Dictionary](entries) with Option_Component {
+ new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component {
name = option_name
tooltip = GUI.tooltip_lines(opt.print_default)
val title = opt.title()