src/Tools/jEdit/src/graphview_dockable.scala

 
 
 import isabelle._
 
 import java.awt.BorderLayout
-import javax.swing.JPanel
+import javax.swing.{JPanel, JComponent}
 
 import scala.actors.Actor._
 
 import org.gjt.sp.jedit.View
 

   // FIXME mutable GUI content
   private def set_graphview(graph: XML.Body)
   {
     graphview.removeAll()
     graphview.setLayout(new BorderLayout)
-    val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
+    val panel =
+      new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
+        override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+        {
+          val rendering = Isabelle_Rendering(current_snapshot, Isabelle.options.value)
+          new Pretty_Tooltip(view, parent, rendering, x, y, body)
+          null
+        }
+      }
     graphview.add(panel.peer, BorderLayout.CENTER)
   }
 
   set_graphview(current_graph)
   set_content(graphview)