equal
deleted
inserted
replaced
103 if path.is_file |
103 if path.is_file |
104 } yield new Dictionary(path) |
104 } yield new Dictionary(path) |
105 |
105 |
106 def dictionaries_selector(): Option_Component = |
106 def dictionaries_selector(): Option_Component = |
107 { |
107 { |
108 Swing_Thread.require() |
108 Swing_Thread.require {} |
109 |
109 |
110 val option_name = "spell_checker_dictionary" |
110 val option_name = "spell_checker_dictionary" |
111 val opt = PIDE.options.value.check_name(option_name) |
111 val opt = PIDE.options.value.check_name(option_name) |
112 |
112 |
113 val entries = dictionaries() |
113 val entries = dictionaries() |