src/Tools/jEdit/src/plugin.scala
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)