# HG changeset patch
# User wenzelm
# Date 1349692835 -7200
# Node ID e0d98ff3c0db70add15d327721f010d674503788
# Parent f53a8f73b40fdb3f2fab633bdc190369026013db
use Pretty_Tooltip for Graphview_Panel;
tuned signature;
diff -r f53a8f73b40f -r e0d98ff3c0db src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala Mon Oct 08 12:02:32 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Mon Oct 08 12:40:35 2012 +0200
@@ -10,13 +10,13 @@
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
import java.awt.geom.{AffineTransform, Point2D}
-import javax.swing.JScrollPane
+import javax.swing.{JScrollPane, JComponent}
import scala.swing.{Panel, ScrollPane}
import scala.swing.event._
-class Graph_Panel(vis: Visualizer, make_tooltip: XML.Body => String)
+class Graph_Panel(vis: Visualizer, make_tooltip: (JComponent, Int, Int, XML.Body) => String)
extends ScrollPane
{
private val panel = this
@@ -24,7 +24,9 @@
private var tooltip_content: XML.Body = Nil
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
- override def getToolTipText(): String = make_tooltip(tooltip_content)
+ override def getToolTipText(event: java.awt.event.MouseEvent): String =
+ if (tooltip_content.isEmpty) null
+ else make_tooltip(panel.peer, event.getX, event.getY, tooltip_content)
}
peer.setWheelScrollingEnabled(false)
diff -r f53a8f73b40f -r e0d98ff3c0db src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala Mon Oct 08 12:02:32 2012 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala Mon Oct 08 12:40:35 2012 +0200
@@ -12,8 +12,10 @@
import scala.collection.JavaConversions._
import scala.swing.{BorderPanel, Button, BoxPanel,
- Orientation, Swing, CheckBox, Action, FileChooser}
+ Orientation, Swing, CheckBox, Action, FileChooser}
+
import javax.swing.border.EmptyBorder
+import javax.swing.JComponent
import java.awt.Dimension
import java.io.File
@@ -21,15 +23,10 @@
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.encode(txt) + "
"
- }
- }
+ def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+ "" +
+ HTML.encode(Pretty.string_of(body)) + "
"
focusable = true
requestFocus()
diff -r f53a8f73b40f -r e0d98ff3c0db src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Oct 08 12:02:32 2012 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Oct 08 12:40:35 2012 +0200
@@ -11,7 +11,7 @@
import isabelle._
import java.awt.BorderLayout
-import javax.swing.JPanel
+import javax.swing.{JPanel, JComponent}
import scala.actors.Actor._
@@ -41,7 +41,15 @@
{
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)
}
diff -r f53a8f73b40f -r e0d98ff3c0db src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Oct 08 12:02:32 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Oct 08 12:40:35 2012 +0200
@@ -23,10 +23,10 @@
class Pretty_Tooltip(
view: View,
- text_area: TextArea,
+ parent: JComponent,
rendering: Isabelle_Rendering,
mouse_x: Int, mouse_y: Int, body: XML.Body)
- extends JWindow(JEdit_Lib.parent_window(text_area) getOrElse view)
+ extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
{
window =>
@@ -115,10 +115,8 @@
}
{
- val container = text_area.getPainter
- val font_metrics = container.getFontMetrics
- val point = new Point(mouse_x, mouse_y + font_metrics.getHeight / 2)
- SwingUtilities.convertPointToScreen(point, container)
+ val point = new Point(mouse_x, mouse_y)
+ SwingUtilities.convertPointToScreen(point, parent)
val screen = Toolkit.getDefaultToolkit.getScreenSize
val x = point.x min (screen.width - window.getWidth)
diff -r f53a8f73b40f -r e0d98ff3c0db src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Oct 08 12:02:32 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Oct 08 12:40:35 2012 +0200
@@ -205,7 +205,11 @@
val tip =
if (control) rendering.tooltip(range)
else rendering.tooltip_message(range)
- if (!tip.isEmpty) new Pretty_Tooltip(view, text_area, rendering, x, y, tip)
+ if (!tip.isEmpty) {
+ val painter = text_area.getPainter
+ val y1 = y + painter.getFontMetrics.getHeight / 2
+ new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+ }
}
null
}