--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 21:47:12 2015 +0100
@@ -78,7 +78,7 @@
override def selection_color = view.getTextArea.getPainter.getSelectionColor
override def error_color = PIDE.options.color_value("error_color")
- override def font() =
+ override def make_font(): Font =
GUI.imitate_font(Font_Info.main().font,
PIDE.options.string("graphview_font_family"),
PIDE.options.real("graphview_font_scale"))