--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 14:13:38 2015 +0100
@@ -10,7 +10,7 @@
import isabelle._
import javax.swing.JComponent
-import java.awt.Point
+import java.awt.{Point, Font}
import java.awt.event.{WindowFocusListener, WindowEvent}
import org.gjt.sp.jedit.View
@@ -62,7 +62,7 @@
graph_result match {
case Exn.Res(graph) =>
val model = new isabelle.graphview.Model(graph)
- val visualizer = new isabelle.graphview.Visualizer(model) {
+ val visualizer = new isabelle.graphview.Visualizer(PIDE.options.value, model) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
Pretty_Tooltip.invoke(() =>
@@ -77,8 +77,11 @@
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
+
+ override def font() =
+ GUI.imitate_font(Font_Info.main().font,
+ PIDE.options.string("graphview_font_family"),
+ PIDE.options.real("graphview_font_scale"))
}
new isabelle.graphview.Main_Panel(model, visualizer)
case Exn.Exn(exn) => new TextArea(Exn.message(exn))