1.1 --- a/src/Tools/Graphview/lib/Tools/graphview	Sun Oct 07 16:26:31 2012 +0200
     1.2 +++ b/src/Tools/Graphview/lib/Tools/graphview	Mon Oct 08 12:02:32 2012 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  ## sources
     1.5  
     1.6  declare -a SOURCES=(
     1.7 -  "src/floating_dialog.scala"
     1.8    "src/graph_panel.scala"
     1.9    "src/graphview.scala"
    1.10    "src/layout_pendulum.scala"

     2.1 --- a/src/Tools/Graphview/src/floating_dialog.scala	Sun Oct 07 16:26:31 2012 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,33 +0,0 @@
     2.4 -/*  Title:      Tools/Graphview/src/floating_dialog.scala
     2.5 -    Author:     Markus Kaiser, TU Muenchen
     2.6 -
     2.7 -PopUp Dialog containing node meta-information.
     2.8 -*/
     2.9 -
    2.10 -package isabelle.graphview
    2.11 -
    2.12 -
    2.13 -import isabelle._
    2.14 -
    2.15 -import scala.swing.{Dialog, BorderPanel, Component, TextArea}
    2.16 -import java.awt.{Font, Point, Dimension}
    2.17 -
    2.18 -
    2.19 -class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
    2.20 -extends Dialog
    2.21 -{    
    2.22 -  location = _location
    2.23 -  title = _title
    2.24 -  //No adaptive size because we don't want to resize the Dialog about 1 sec
    2.25 -  //after it is shown.
    2.26 -  preferredSize = new Dimension(300, 300)
    2.27 -  peer.setAlwaysOnTop(true)
    2.28 -
    2.29 -  private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
    2.30 -  private val text = new TextArea
    2.31 -  text.peer.setFont(text_font)
    2.32 -  text.editable = false
    2.33 -
    2.34 -  contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
    2.35 -  text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
    2.36 -}

     3.1 --- a/src/Tools/Graphview/src/graph_panel.scala	Sun Oct 07 16:26:31 2012 +0200
     3.2 +++ b/src/Tools/Graphview/src/graph_panel.scala	Mon Oct 08 12:02:32 2012 +0200
     3.3 @@ -10,19 +10,30 @@
     3.4  
     3.5  import java.awt.{Dimension, Graphics2D, Point, Rectangle}
     3.6  import java.awt.geom.{AffineTransform, Point2D}
     3.7 -import javax.swing.ToolTipManager
     3.8 +import javax.swing.JScrollPane
     3.9 +
    3.10  import scala.swing.{Panel, ScrollPane}
    3.11  import scala.swing.event._
    3.12  
    3.13  
    3.14 -class Graph_Panel(private val vis: Visualizer) extends ScrollPane {
    3.15 -  this.peer.setWheelScrollingEnabled(false)
    3.16 +class Graph_Panel(vis: Visualizer, make_tooltip: XML.Body => String)
    3.17 +  extends ScrollPane
    3.18 +{
    3.19 +  private val panel = this
    3.20 +
    3.21 +  private var tooltip_content: XML.Body = Nil
    3.22 +
    3.23 +  override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
    3.24 +    override def getToolTipText(): String = make_tooltip(tooltip_content)
    3.25 +  }
    3.26 +
    3.27 +  peer.setWheelScrollingEnabled(false)
    3.28    focusable = true
    3.29    requestFocus()
    3.30    
    3.31    horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
    3.32    verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
    3.33 -  
    3.34 +
    3.35    def visualizer = vis
    3.36    
    3.37    def fit_to_window() = {
    3.38 @@ -82,7 +93,6 @@
    3.39    }
    3.40    vis.model.Colors.events += r
    3.41    vis.model.Mutators.events += r
    3.42 -  ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
    3.43    
    3.44    apply_layout()
    3.45    fit_to_window()
    3.46 @@ -126,7 +136,6 @@
    3.47      }
    3.48    }
    3.49    
    3.50 -  private val panel = this
    3.51    object Interaction {
    3.52      object Keyboard {
    3.53        import scala.swing.event.Key._
    3.54 @@ -203,8 +212,8 @@
    3.55        def moved(at: Point) {
    3.56          val c = Transform.pane_to_graph_coordinates(at)
    3.57          node(c) match {
    3.58 -          case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
    3.59 -          case None => panel.tooltip = null
    3.60 +          case Some(l) => panel.tooltip = ""; panel.tooltip_content = vis.Tooltip.content(l)
    3.61 +          case None => panel.tooltip = null; panel.tooltip_content = Nil
    3.62          }
    3.63        }
    3.64        
    3.65 @@ -254,27 +263,9 @@
    3.66            menu.show(panel.peer, at.x, at.y)
    3.67          }
    3.68          
    3.69 -        def double_click() {
    3.70 -          p match {
    3.71 -            case Some(l) => {
    3.72 -                val p = at.clone.asInstanceOf[Point]
    3.73 -                SwingUtilities.convertPointToScreen(p, panel.peer)
    3.74 -                new Floating_Dialog(
    3.75 -                  vis.Tooltip.content(l),
    3.76 -                  vis.Caption(l),
    3.77 -                  at
    3.78 -                ).open
    3.79 -            }
    3.80 -            
    3.81 -            case None =>
    3.82 -          }          
    3.83 -        }
    3.84 -        
    3.85          if (clicks < 2) {
    3.86            if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
    3.87            else left_click()
    3.88 -        } else if (clicks == 2) {
    3.89 -          if (SwingUtilities.isLeftMouseButton(e.peer)) double_click()
    3.90          }
    3.91        }   
    3.92  

     4.1 --- a/src/Tools/Graphview/src/graphview.scala	Sun Oct 07 16:26:31 2012 +0200
     4.2 +++ b/src/Tools/Graphview/src/graphview.scala	Mon Oct 08 12:02:32 2012 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4  import java.awt.Dimension
     4.5  import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
     4.6  import javax.swing.border.EmptyBorder
     4.7 +import javax.swing.ToolTipManager
     4.8  
     4.9  
    4.10  object Graphview extends SwingApplication
    4.11 @@ -24,6 +25,7 @@
    4.12          Platform.init_laf()
    4.13          Isabelle_System.init()
    4.14          Isabelle_System.install_fonts()
    4.15 +        ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
    4.16  
    4.17          args.toList match {
    4.18            case List(arg) =>

     5.1 --- a/src/Tools/Graphview/src/main_panel.scala	Sun Oct 07 16:26:31 2012 +0200
     5.2 +++ b/src/Tools/Graphview/src/main_panel.scala	Mon Oct 08 12:02:32 2012 +0200
     5.3 @@ -18,14 +18,25 @@
     5.4  import java.io.File
     5.5  
     5.6  
     5.7 -class Main_Panel(graph: Model.Graph) extends BorderPanel
     5.8 +class Main_Panel(graph: Model.Graph)
     5.9 +  extends BorderPanel
    5.10  {
    5.11 +  def make_tooltip(body: XML.Body): String =
    5.12 +  {
    5.13 +    if (body.isEmpty) null
    5.14 +    else {
    5.15 +      val txt = Pretty.string_of(body)
    5.16 +      "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
    5.17 +          Parameters.tooltip_font_size + "px; \">" + HTML.encode(txt) + "</pre></html>"
    5.18 +    }
    5.19 +  }
    5.20 +
    5.21    focusable = true
    5.22    requestFocus()
    5.23    
    5.24    val model = new Model(graph)
    5.25    val visualizer = new Visualizer(model)
    5.26 -  val graph_panel = new Graph_Panel(visualizer)
    5.27 +  val graph_panel = new Graph_Panel(visualizer, make_tooltip)
    5.28    
    5.29    listenTo(keys)
    5.30    reactions += graph_panel.reactions

     6.1 --- a/src/Tools/Graphview/src/parameters.scala	Sun Oct 07 16:26:31 2012 +0200
     6.2 +++ b/src/Tools/Graphview/src/parameters.scala	Mon Oct 08 12:02:32 2012 +0200
     6.3 @@ -15,6 +15,8 @@
     6.4  {
     6.5    val font_family: String = "IsabelleText"
     6.6    val font_size: Int = 16
     6.7 +  val tooltip_font_size: Int = 10
     6.8 +
     6.9  
    6.10    object Colors {
    6.11      val Filter_Colors = List(

     7.1 --- a/src/Tools/Graphview/src/visualizer.scala	Sun Oct 07 16:26:31 2012 +0200
     7.2 +++ b/src/Tools/Graphview/src/visualizer.scala	Mon Oct 08 12:02:32 2012 +0200
     7.3 @@ -9,6 +9,7 @@
     7.4  import isabelle._
     7.5  
     7.6  import java.awt.{RenderingHints, Graphics2D}
     7.7 +import javax.swing.JComponent
     7.8  
     7.9  
    7.10  class Visualizer(val model: Model) {
    7.11 @@ -143,18 +144,8 @@
    7.12    
    7.13    object Tooltip {
    7.14      def content(name: String): XML.Body = model.complete.get_node(name).content
    7.15 +  }
    7.16  
    7.17 -    def text(name: String, fm: java.awt.FontMetrics): String = // null
    7.18 -    {
    7.19 -      val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
    7.20 -      if (txt == "") null
    7.21 -      else
    7.22 -        "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
    7.23 -            Parameters.font_size + "px; \">" +  // FIXME proper scaling (!?)
    7.24 -          HTML.encode(txt) + "</pre></html>"
    7.25 -    }
    7.26 -  }
    7.27 -  
    7.28    object Font {
    7.29      import java.awt.{Font => awtFont}
    7.30