# HG changeset patch
# User wenzelm
# Date 1420142947 -3600
# Node ID 876a81f5788bb1b3f1df4b32d368d3f715353d19
# Parent  07a7dfd6d694cab8cb32d163f6d5d7fd42484994
tuned signature;

diff -r 07a7dfd6d694 -r 876a81f5788b src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 21:01:18 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 21:09:07 2015 +0100
@@ -19,10 +19,7 @@
   MouseMoved, MouseClicked, MouseWheelMoved, MouseEvent}
 
 
-class Graph_Panel(
-    val visualizer: Visualizer,
-    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
-  extends ScrollPane
+class Graph_Panel(val visualizer: Visualizer) extends ScrollPane
 {
   panel =>
 
@@ -32,7 +29,7 @@
         case Some(name) =>
           visualizer.model.complete_graph.get_node(name).content match {
             case Nil => null
-            case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+            case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
           }
         case None => null
       }
diff -r 07a7dfd6d694 -r 876a81f5788b src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Thu Jan 01 21:01:18 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Thu Jan 01 21:09:07 2015 +0100
@@ -25,8 +25,7 @@
   focusable = true
   requestFocus()
 
-  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
-  val graph_panel = new Graph_Panel(visualizer, make_tooltip)
+  val graph_panel = new Graph_Panel(visualizer)
 
   listenTo(keys)
   reactions += graph_panel.reactions
diff -r 07a7dfd6d694 -r 876a81f5788b src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Thu Jan 01 21:01:18 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Thu Jan 01 21:09:07 2015 +0100
@@ -20,6 +20,11 @@
   visualizer =>
 
 
+  /* tooltips */
+
+  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
+
+
   /* main colors */
 
   def foreground_color: Color = Color.BLACK
diff -r 07a7dfd6d694 -r 876a81f5788b src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 21:01:18 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 21:09:07 2015 +0100
@@ -63,14 +63,6 @@
       case Exn.Res(graph) =>
         val model = new isabelle.graphview.Model(graph)
         val visualizer = new isabelle.graphview.Visualizer(model) {
-          override def foreground_color = view.getTextArea.getPainter.getForeground
-          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 =
           {
             Pretty_Tooltip.invoke(() =>
@@ -81,7 +73,14 @@
               })
             null
           }
+          override def foreground_color = view.getTextArea.getPainter.getForeground
+          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)
       case Exn.Exn(exn) => new TextArea(Exn.message(exn))
     }
   set_content(graphview)