changeset 69377 | 81ae5893c556 |
parent 69255 | 800b1ce96fce |
child 69458 | 5655af3ea5bd |
--- a/src/Tools/jEdit/src/plugin.scala Fri Nov 30 14:21:28 2018 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Fri Nov 30 14:46:00 2018 +0100 @@ -399,6 +399,8 @@ if (buffer != null && text_area != null) init_view(buffer, text_area) } + GUI.use_isabelle_fonts() + spell_checker.update(options.value) session.update_options(options.value)