--- a/src/Tools/Graphview/lib/Tools/graphview Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview Mon Oct 08 12:02:32 2012 +0200
@@ -8,7 +8,6 @@
## sources
declare -a SOURCES=(
- "src/floating_dialog.scala"
"src/graph_panel.scala"
"src/graphview.scala"
"src/layout_pendulum.scala"
--- a/src/Tools/Graphview/src/floating_dialog.scala Sun Oct 07 16:26:31 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/* Title: Tools/Graphview/src/floating_dialog.scala
- Author: Markus Kaiser, TU Muenchen
-
-PopUp Dialog containing node meta-information.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import scala.swing.{Dialog, BorderPanel, Component, TextArea}
-import java.awt.{Font, Point, Dimension}
-
-
-class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
-extends Dialog
-{
- location = _location
- title = _title
- //No adaptive size because we don't want to resize the Dialog about 1 sec
- //after it is shown.
- preferredSize = new Dimension(300, 300)
- peer.setAlwaysOnTop(true)
-
- private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
- private val text = new TextArea
- text.peer.setFont(text_font)
- text.editable = false
-
- contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
- text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
-}
--- a/src/Tools/Graphview/src/graph_panel.scala Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Mon Oct 08 12:02:32 2012 +0200
@@ -10,19 +10,30 @@
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
import java.awt.geom.{AffineTransform, Point2D}
-import javax.swing.ToolTipManager
+import javax.swing.JScrollPane
+
import scala.swing.{Panel, ScrollPane}
import scala.swing.event._
-class Graph_Panel(private val vis: Visualizer) extends ScrollPane {
- this.peer.setWheelScrollingEnabled(false)
+class Graph_Panel(vis: Visualizer, make_tooltip: XML.Body => String)
+ extends ScrollPane
+{
+ private val panel = this
+
+ private var tooltip_content: XML.Body = Nil
+
+ override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
+ override def getToolTipText(): String = make_tooltip(tooltip_content)
+ }
+
+ peer.setWheelScrollingEnabled(false)
focusable = true
requestFocus()
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-
+
def visualizer = vis
def fit_to_window() = {
@@ -82,7 +93,6 @@
}
vis.model.Colors.events += r
vis.model.Mutators.events += r
- ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
apply_layout()
fit_to_window()
@@ -126,7 +136,6 @@
}
}
- private val panel = this
object Interaction {
object Keyboard {
import scala.swing.event.Key._
@@ -203,8 +212,8 @@
def moved(at: Point) {
val c = Transform.pane_to_graph_coordinates(at)
node(c) match {
- case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
- case None => panel.tooltip = null
+ case Some(l) => panel.tooltip = ""; panel.tooltip_content = vis.Tooltip.content(l)
+ case None => panel.tooltip = null; panel.tooltip_content = Nil
}
}
@@ -254,27 +263,9 @@
menu.show(panel.peer, at.x, at.y)
}
- def double_click() {
- p match {
- case Some(l) => {
- val p = at.clone.asInstanceOf[Point]
- SwingUtilities.convertPointToScreen(p, panel.peer)
- new Floating_Dialog(
- vis.Tooltip.content(l),
- vis.Caption(l),
- at
- ).open
- }
-
- case None =>
- }
- }
-
if (clicks < 2) {
if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
else left_click()
- } else if (clicks == 2) {
- if (SwingUtilities.isLeftMouseButton(e.peer)) double_click()
}
}
--- 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) =>
--- a/src/Tools/Graphview/src/main_panel.scala Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala Mon Oct 08 12:02:32 2012 +0200
@@ -18,14 +18,25 @@
import java.io.File
-class Main_Panel(graph: Model.Graph) extends BorderPanel
+class Main_Panel(graph: Model.Graph)
+ extends BorderPanel
{
+ def make_tooltip(body: XML.Body): String =
+ {
+ if (body.isEmpty) null
+ else {
+ val txt = Pretty.string_of(body)
+ "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
+ Parameters.tooltip_font_size + "px; \">" + HTML.encode(txt) + "</pre></html>"
+ }
+ }
+
focusable = true
requestFocus()
val model = new Model(graph)
val visualizer = new Visualizer(model)
- val graph_panel = new Graph_Panel(visualizer)
+ val graph_panel = new Graph_Panel(visualizer, make_tooltip)
listenTo(keys)
reactions += graph_panel.reactions
--- a/src/Tools/Graphview/src/parameters.scala Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/src/parameters.scala Mon Oct 08 12:02:32 2012 +0200
@@ -15,6 +15,8 @@
{
val font_family: String = "IsabelleText"
val font_size: Int = 16
+ val tooltip_font_size: Int = 10
+
object Colors {
val Filter_Colors = List(
--- a/src/Tools/Graphview/src/visualizer.scala Sun Oct 07 16:26:31 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala Mon Oct 08 12:02:32 2012 +0200
@@ -9,6 +9,7 @@
import isabelle._
import java.awt.{RenderingHints, Graphics2D}
+import javax.swing.JComponent
class Visualizer(val model: Model) {
@@ -143,18 +144,8 @@
object Tooltip {
def content(name: String): XML.Body = model.complete.get_node(name).content
+ }
- def text(name: String, fm: java.awt.FontMetrics): String = // null
- {
- val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
- if (txt == "") null
- else
- "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
- Parameters.font_size + "px; \">" + // FIXME proper scaling (!?)
- HTML.encode(txt) + "</pre></html>"
- }
- }
-
object Font {
import java.awt.{Font => awtFont}