# HG changeset patch
# User wenzelm
# Date 1543409969 -3600
# Node ID 3b709d9074ec8d13acdb8a097ed6591c49db9ab9
# Parent  71ef6e6da3dc92e852c9b8196890e0bb8d21319d
prefer Isabelle_Fonts.sans for GUI;

diff -r 71ef6e6da3dc -r 3b709d9074ec 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"),