# HG changeset patch
# User wenzelm
# Date 1421605270 -3600
# Node ID 4c5396f52546f30ba3fb45d14e6c84af38f8bf13
# Parent  bc3a21ca23aafc1c45e36bfba4a37eae08c9b422
tuned signature;

diff -r bc3a21ca23aa -r 4c5396f52546 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Sun Jan 18 19:21:10 2015 +0100
@@ -34,7 +34,7 @@
   }
 
   val split_pane =
-    if (visualizer.get_options.bool("graphview_swap_panels"))
+    if (visualizer.options.bool("graphview_swap_panels"))
       new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
     else
       new SplitPane(Orientation.Vertical, graph_panel, tree_panel)
diff -r bc3a21ca23aa -r 4c5396f52546 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 19:21:10 2015 +0100
@@ -84,7 +84,7 @@
   private val selection_field_foreground = selection_field.foreground
 
   private val selection_delay =
-    GUI_Thread.delay_last(visualizer.get_options.seconds("editor_input_delay")) {
+    GUI_Thread.delay_last(visualizer.options.seconds("editor_input_delay")) {
       val (pattern, ok) =
         selection_field.text match {
           case null | "" => (None, true)
diff -r bc3a21ca23aa -r 4c5396f52546 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 18 19:21:10 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Markus Kaiser, TU Muenchen
     Author:     Makarius
 
-Graph visualization parameters and interface state.
+Graph visualization parameters and GUI state.
 */
 
 package isabelle.graphview
@@ -15,12 +15,12 @@
 import javax.swing.JComponent
 
 
-class Visualizer(options: => Options, val model: Model)
+abstract class Visualizer(val model: Model)
 {
   visualizer =>
 
 
-  def get_options: Options = options
+  def options: Options
 
 
   /* layout state */
diff -r bc3a21ca23aa -r 4c5396f52546 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Jan 18 19:21:10 2015 +0100
@@ -62,26 +62,29 @@
     graph_result match {
       case Exn.Res(graph) =>
         val model = new isabelle.graphview.Model(graph)
-        val visualizer = new isabelle.graphview.Visualizer(PIDE.options.value, model) {
+        val visualizer = new isabelle.graphview.Visualizer(model) {
+          def options: Options = PIDE.options.value
+
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             Pretty_Tooltip.invoke(() =>
               {
-                val rendering = Rendering(snapshot, PIDE.options.value)
+                val rendering = Rendering(snapshot, options)
                 val info = Text.Info(Text.Range(~1), body)
                 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
               })
             null
           }
+
+          override def make_font(): Font =
+            GUI.imitate_font(Font_Info.main().font,
+              options.string("graphview_font_family"),
+              options.real("graphview_font_scale"))
+
           override def foreground_color = view.getTextArea.getPainter.getForeground
           override def selection_color = view.getTextArea.getPainter.getSelectionColor
           override def current_color = view.getTextArea.getPainter.getLineHighlightColor
           override def error_color = PIDE.options.color_value("error_color")
-
-          override def make_font(): 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))