src/Tools/Graphview/src/graphview.scala

--- a/src/Tools/Graphview/src/graphview.scala	Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Mon Oct 08 12:02:32 2012 +0200
@@ -12,6 +12,7 @@
 import java.awt.Dimension
 import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
 import javax.swing.border.EmptyBorder
+import javax.swing.ToolTipManager
 
 
 object Graphview extends SwingApplication
@@ -24,6 +25,7 @@
         Platform.init_laf()
         Isabelle_System.init()
         Isabelle_System.install_fonts()
+        ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
 
         args.toList match {
           case List(arg) =>