--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Jan 01 17:27:52 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Thu Jan 01 20:50:20 2015 +0100
@@ -67,6 +67,8 @@
override def background_color = view.getTextArea.getPainter.getBackground
override def selection_color = view.getTextArea.getPainter.getSelectionColor
override def error_color = PIDE.options.color_value("error_color")
+ override def font_size = view.getTextArea.getPainter.getFont.getSize
+ override def font = view.getTextArea.getPainter.getFont
}
new isabelle.graphview.Main_Panel(model, visualizer) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =