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