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