prefer Isabelle_Fonts.sans for GUI;
authorwenzelm
Wed, 28 Nov 2018 13:59:29 +0100
changeset 69359 3b709d9074ec
parent 69358 71ef6e6da3dc
child 69360 dc9a39c3f75d
prefer Isabelle_Fonts.sans for GUI;
src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Nov 28 12:05:50 2018 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Nov 28 13:59:29 2018 +0100
@@ -78,7 +78,7 @@
           }
 
           override def make_font(): Font =
-            if (editor_style) Font_Info.main(PIDE.options.real("graphview_font_scale")).font
+            if (editor_style) GUI.imitate_font(Font_Info.main().font)
             else
               GUI.imitate_font(Font_Info.main().font,
                 family = options.string("graphview_font_family"),