--- a/src/Tools/Graphview/lib/Tools/graphview Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview Tue Oct 09 11:51:06 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 Tue Oct 09 00:40:33 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 Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Tue Oct 09 11:51:06 2012 +0200
@@ -10,31 +10,66 @@
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
import java.awt.geom.{AffineTransform, Point2D}
-import javax.swing.ToolTipManager
+import java.awt.image.BufferedImage
+import javax.swing.{JScrollPane, JComponent}
+
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(
+ val visualizer: Visualizer,
+ make_tooltip: (JComponent, Int, Int, XML.Body) => String)
+ extends ScrollPane
+{
+ panel =>
+
+ tooltip = ""
+
+ override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
+ override def getToolTipText(event: java.awt.event.MouseEvent): String =
+ node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+ case Some(name) =>
+ visualizer.model.complete.get_node(name).content match {
+ case Nil => null
+ case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+ }
+ case None => null
+ }
+ }
+
+ peer.setWheelScrollingEnabled(false)
focusable = true
requestFocus()
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-
- def visualizer = vis
-
+
+ private val gfx_aux =
+ new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
+ gfx_aux.setFont(visualizer.Font())
+ gfx_aux.setRenderingHints(visualizer.rendering_hints)
+
+ def node(at: Point2D): Option[String] =
+ visualizer.model.visible_nodes()
+ .find(name => visualizer.Drawer.shape(gfx_aux, Some(name)).contains(at))
+
+ def refresh()
+ {
+ paint_panel.set_preferred_size()
+ paint_panel.repaint()
+ }
+
def fit_to_window() = {
Transform.fit_to_window()
- repaint()
+ refresh()
}
- def apply_layout() = vis.Coordinates.layout()
+ def apply_layout() = visualizer.Coordinates.layout()
private val paint_panel = new Panel {
def set_preferred_size() {
- val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+ val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
val s = Transform.scale
val (px, py) = Transform.padding
@@ -45,11 +80,10 @@
}
override def paint(g: Graphics2D) {
- set_preferred_size()
super.paintComponent(g)
g.transform(Transform())
- vis.Drawer.paint_all_visible(g, true)
+ visualizer.Drawer.paint_all_visible(g, true)
}
}
contents = paint_panel
@@ -68,21 +102,9 @@
case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
case MouseMoved(_, _, _) => repaint()
}
- private val r = {
- import scala.actors.Actor._
-
- actor {
- loop {
- react {
- // FIXME Swing thread!?
- case _ => repaint()
- }
- }
- }
- }
- vis.model.Colors.events += r
- vis.model.Mutators.events += r
- ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
+
+ visualizer.model.Colors.events += { case _ => repaint() }
+ visualizer.model.Mutators.events += { case _ => repaint() }
apply_layout()
fit_to_window()
@@ -98,7 +120,7 @@
}
def apply() = {
- val (minX, minY, _, _) = vis.Coordinates.bounds()
+ val (minX, minY, _, _) = visualizer.Coordinates.bounds()
val at = AffineTransform.getScaleInstance(scale, scale)
at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
@@ -106,10 +128,10 @@
}
def fit_to_window() {
- if (vis.model.visible_nodes().isEmpty)
+ if (visualizer.model.visible_nodes().isEmpty)
scale = 1
else {
- val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+ val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
val (sx, sy) = (1d * size.width / dx, 1d * size.height / dy)
@@ -126,7 +148,6 @@
}
}
- private val panel = this
object Interaction {
object Keyboard {
import scala.swing.event.Key._
@@ -149,7 +170,7 @@
}
case('1', _) => {
- vis.Coordinates.layout()
+ visualizer.Coordinates.layout()
}
case('2', _) => {
@@ -161,16 +182,11 @@
}
object Mouse {
- import java.awt.image.BufferedImage
import scala.swing.event.Key.Modifier._
type Modifiers = Int
type Dummy = ((String, String), Int)
private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
- private val g =
- new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
- g.setFont(vis.Font())
- g.setRenderingHints(vis.rendering_hints)
val react: PartialFunction[Event, Unit] = {
case MousePressed(_, p, _, _, _) => pressed(p)
@@ -181,41 +197,24 @@
}
case MouseWheelMoved(_, p, _, r) => wheel(r, p)
case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
- case MouseMoved(_, p, _) => moved(p)
}
- def node(at: Point2D): Option[String] =
- vis.model.visible_nodes().find({
- l => vis.Drawer.shape(g, Some(l)).contains(at)
- })
-
def dummy(at: Point2D): Option[Dummy] =
- vis.model.visible_edges().map({
- i => vis.Coordinates(i).zipWithIndex.map((i, _))
+ visualizer.model.visible_edges().map({
+ i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
}).flatten.find({
case (_, ((x, y), _)) =>
- vis.Drawer.shape(g, None).contains(at.getX() - x, at.getY() - y)
+ visualizer.Drawer.shape(gfx_aux, None).contains(at.getX() - x, at.getY() - y)
}) match {
case None => None
case Some((name, (_, index))) => Some((name, index))
}
- 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
- }
- }
-
def pressed(at: Point) {
val c = Transform.pane_to_graph_coordinates(at)
val l = node(c) match {
- case Some(l) => if (vis.Selection(l))
- vis.Selection()
- else
- List(l)
-
+ case Some(l) =>
+ if (visualizer.Selection(l)) visualizer.Selection() else List(l)
case None => Nil
}
val d = l match {
@@ -238,43 +237,25 @@
def left_click() {
(p, m) match {
- case (Some(l), Control) => vis.Selection.add(l)
+ case (Some(l), Control) => visualizer.Selection.add(l)
case (None, Control) =>
- case (Some(l), Shift) => vis.Selection.add(l)
+ case (Some(l), Shift) => visualizer.Selection.add(l)
case (None, Shift) =>
- case (Some(l), _) => vis.Selection.set(List(l))
- case (None, _) => vis.Selection.clear
+ case (Some(l), _) => visualizer.Selection.set(List(l))
+ case (None, _) => visualizer.Selection.clear
}
}
def right_click() {
- val menu = Popups(panel, p, vis.Selection())
+ val menu = Popups(panel, p, visualizer.Selection())
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()
}
}
@@ -292,10 +273,10 @@
}
case (Nil, ds) =>
- ds.foreach(d => vis.Coordinates.translate(d, (dx / s, dy / s)))
+ ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
case (ls, _) =>
- ls.foreach(l => vis.Coordinates.translate(l, (dx / s, dy / s)))
+ ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
}
}
--- a/src/Tools/Graphview/src/graphview.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/graphview.scala Tue Oct 09 11:51:06 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/layout_pendulum.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala Tue Oct 09 11:51:06 2012 +0200
@@ -22,12 +22,15 @@
val x_distance = 350
val y_distance = 350
val pendulum_iterations = 10
+ val minimize_crossings_iterations = 40
- def apply(graph: Model.Graph): Layout = {
- if (graph.entries.isEmpty)
+ def apply(graph: Model.Graph): Layout =
+ {
+ if (graph.is_empty)
(Map[Key, Point](), Map[(Key, Key), List[Point]]())
else {
- val (dummy_graph, dummies, dummy_levels) = {
+ val (dummy_graph, dummies, dummy_levels) =
+ {
val initial_levels = level_map(graph)
def add_dummies(graph: Model.Graph, from: Key, to: Key,
@@ -79,7 +82,7 @@
initial_coordinates(levels)
)
- val dummy_coords =
+ val dummy_coords =
(Map[(Key, Key), List[Point]]() /: dummies.keys) {
case (map, key) => map + (key -> dummies(key).map(coords(_)))
}
@@ -87,32 +90,30 @@
(coords, dummy_coords)
}
}
-
+
def level_map(graph: Model.Graph): Map[Key, Int] =
- (Map[Key, Int]() /: graph.topological_order){
+ (Map[Key, Int]() /: graph.topological_order) {
(levels, key) => {
- val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
- levels + (key -> (pred_levels.max + 1))
- }}
+ val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
+ levels + (key -> lev)
+ }
+ }
def level_list(map: Map[Key, Int]): Levels =
- (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
- case ((key, i), list) => {
- if (list.isEmpty) (i, List(key)) :: list
- else {
- val (j, l) = list.head
- if (i == j) (i, key :: l) :: list.tail
- else (i, List(key)) :: list
- }
- }
- }.map(_._2)
-
+ {
+ val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
+ val buckets = new Array[Level](max_lev + 1)
+ for (l <- 0 to max_lev) { buckets(l) = Nil }
+ for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
+ buckets.iterator.map(_.sorted).toList
+ }
+
def count_crossings(graph: Model.Graph, levels: Levels): Int = {
def in_level(ls: Levels): Int = ls match {
case List(top, bot) =>
top.zipWithIndex.map{
case (outer_parent, outer_parent_index) =>
- graph.imm_succs(outer_parent).map(bot.indexOf(_))
+ graph.imm_succs(outer_parent).map(bot.indexOf(_)) // FIXME iterator
.map(outer_child => {
(0 until outer_parent_index)
.map(inner_parent =>
@@ -153,11 +154,11 @@
}
}
- ((levels, count_crossings(graph, levels), true) /: (1 to 40)) {
+ ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
case ((old_levels, old_crossings, top_down), _) => {
val new_levels = resort(old_levels, top_down)
val new_crossings = count_crossings(graph, new_levels)
- if ( new_crossings < old_crossings)
+ if (new_crossings < old_crossings)
(new_levels, new_crossings, !top_down)
else
(old_levels, old_crossings, !top_down)
@@ -250,7 +251,7 @@
val regions = levels.map(level => level.map(new Region(graph, _)))
((regions, coords, true, true) /: (1 to pendulum_iterations)) {
- case ((regions, coords, top_down, moved), _) =>
+ case ((regions, coords, top_down, moved), i) =>
if (moved) {
val (nextr, nextc, m) = iteration(regions, coords, top_down)
(nextr, nextc, !top_down, m)
@@ -272,7 +273,7 @@
def deflection(coords: Coordinates, use_preds: Boolean) =
nodes.map(k => (coords(k)._1,
- if (use_preds) graph.imm_preds(k).toList
+ if (use_preds) graph.imm_preds(k).toList // FIXME iterator
else graph.imm_succs(k).toList))
.map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
.sum / nodes.length
--- a/src/Tools/Graphview/src/main_panel.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala Tue Oct 09 11:51:06 2012 +0200
@@ -12,20 +12,31 @@
import scala.collection.JavaConversions._
import scala.swing.{BorderPanel, Button, BoxPanel,
- Orientation, Swing, CheckBox, Action, FileChooser}
+ Orientation, Swing, CheckBox, Action, FileChooser}
+
+import java.io.File
+import java.awt.{Color, Dimension}
+import java.awt.geom.Rectangle2D
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
import javax.swing.border.EmptyBorder
-import java.awt.Dimension
-import java.io.File
+import javax.swing.JComponent
-class Main_Panel(graph: Model.Graph) extends BorderPanel
+class Main_Panel(graph: Model.Graph)
+ extends BorderPanel
{
+ def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
+ "<html><pre style=\"font-family: " + Parameters.font_family +
+ "; font-size: " + Parameters.tooltip_font_size + "px; \">" +
+ HTML.encode(Pretty.string_of(body)) + "</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
@@ -107,11 +118,6 @@
add(options_panel, BorderPanel.Position.North)
private def export(file: File) {
- import java.awt.image.BufferedImage
- import javax.imageio.ImageIO
- import java.awt.geom.Rectangle2D
- import java.awt.Color
-
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
(math.abs(maxY - minY) + 200).toInt,
@@ -124,10 +130,7 @@
visualizer.Drawer.paint_all_visible(g, false)
g.dispose()
- try {
- ImageIO.write(img, "png", file)
- } catch {
- case ex: Exception => ex.printStackTrace
- }
+ try { ImageIO.write(img, "png", file) }
+ catch { case ex: Exception => ex.printStackTrace } // FIXME !?
}
}
--- a/src/Tools/Graphview/src/model.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/model.scala Tue Oct 09 11:51:06 2012 +0200
@@ -10,14 +10,12 @@
import isabelle._
import isabelle.graphview.Mutators._
import java.awt.Color
-import scala.actors.Actor
-import scala.actors.Actor._
class Mutator_Container(val available: List[Mutator]) {
type Mutator_Markup = (Boolean, Color, Mutator)
- val events = new Event_Bus[Mutator_Event.Message]
+ val events = new Mutator_Event.Bus
private var _mutators : List[Mutator_Markup] = Nil
def apply() = _mutators
@@ -80,7 +78,7 @@
def visible_nodes(): Iterator[String] = current.keys
def visible_edges(): Iterator[(String, String)] =
- current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
+ current.keys.map(k => current.imm_succs(k).map((k, _))).flatten // FIXME iterator
def complete = graph
def current: Model.Graph =
@@ -103,11 +101,5 @@
}
})
}
- Colors.events += actor {
- loop {
- react {
- case _ => build_colors()
- }
- }
- }
+ Colors.events += { case _ => build_colors() }
}
\ No newline at end of file
--- a/src/Tools/Graphview/src/mutator.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator.scala Tue Oct 09 11:51:06 2012 +0200
@@ -139,7 +139,7 @@
"Hide transitive edges",
"Hides all transitive edges.",
(g, s, d) => {
- !g.imm_succs(s).filter(_ != d)
+ !g.imm_succs(s).filter(_ != d) // FIXME iterator
.exists(p => !(g.irreducible_paths(p, d).isEmpty))
}
)
--- a/src/Tools/Graphview/src/mutator_dialog.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Tue Oct 09 11:51:06 2012 +0200
@@ -14,16 +14,15 @@
import javax.swing.border.EmptyBorder
import scala.collection.JavaConversions._
import scala.swing._
-import scala.actors.Actor
-import scala.actors.Actor._
import isabelle.graphview.Mutators._
import scala.swing.event.ValueChanged
class Mutator_Dialog(
- container: Mutator_Container, caption: String,
- reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
-extends Dialog
+ container: Mutator_Container, caption: String,
+ reverse_caption: String = "Inverse",
+ show_color_chooser: Boolean = true)
+ extends Dialog
{
type Mutator_Markup = (Boolean, Color, Mutator)
@@ -36,15 +35,9 @@
paintPanels
}
- container.events += actor {
- loop {
- react {
- case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
- case Mutator_Event.NewList(ms) => {
- panels = getPanels(ms)
- }
- }
- }
+ container.events += {
+ case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+ case Mutator_Event.NewList(ms) => panels = getPanels(ms)
}
override def open() {
--- a/src/Tools/Graphview/src/mutator_event.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala Tue Oct 09 11:51:06 2012 +0200
@@ -7,14 +7,29 @@
package isabelle.graphview
+import isabelle._
+
+import scala.collection.mutable
+
import java.awt.Color
object Mutator_Event
{
type Mutator_Markup = (Boolean, Color, Mutator)
-
+
sealed abstract class Message
case class Add(m: Mutator_Markup) extends Message
case class NewList(m: List[Mutator_Markup]) extends Message
+
+ type Receiver = PartialFunction[Message, Unit]
+
+ class Bus
+ {
+ private val receivers = new mutable.ListBuffer[Receiver]
+
+ def += (r: Receiver) { Swing_Thread.require(); receivers += r }
+ def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
+ def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+ }
}
\ No newline at end of file
--- a/src/Tools/Graphview/src/parameters.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/parameters.scala Tue Oct 09 11:51:06 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(
@@ -40,6 +42,6 @@
val No_Axioms = Color.LIGHT_GRAY
}
- var long_names = true
+ var long_names = false
var arrow_heads = false
}
--- a/src/Tools/Graphview/src/popups.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/popups.scala Tue Oct 09 11:51:06 2012 +0200
@@ -61,9 +61,9 @@
if (edges) {
- val outs = ls.map(l => (l, curr.imm_succs(l)))
+ val outs = ls.map(l => (l, curr.imm_succs(l))) // FIXME iterator
.filter(_._2.size > 0).sortBy(_._1)
- val ins = ls.map(l => (l, curr.imm_preds(l)))
+ val ins = ls.map(l => (l, curr.imm_preds(l))) // FIXME iterator
.filter(_._2.size > 0).sortBy(_._1)
if (outs.nonEmpty || ins.nonEmpty) {
--- a/src/Tools/Graphview/src/visualizer.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala Tue Oct 09 11:51:06 2012 +0200
@@ -9,6 +9,7 @@
import isabelle._
import java.awt.{RenderingHints, Graphics2D}
+import javax.swing.JComponent
class Visualizer(val model: Model) {
@@ -136,23 +137,9 @@
}
object Caption {
- def apply(k: String) =
- if (Parameters.long_names) k
- else k.split('.').last
- }
-
- 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>"
- }
+ def apply(key: String) =
+ if (Parameters.long_names) key
+ else model.complete.get_node(key).name
}
object Font {
--- a/src/Tools/jEdit/src/graphview_dockable.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Tue Oct 09 11:51:06 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._
@@ -37,15 +37,24 @@
private val graphview = new JPanel
// FIXME mutable GUI content
- private def set_graphview(graph: XML.Body)
+ private def set_graphview(snapshot: Document.Snapshot, 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(snapshot, Isabelle.options.value)
+ new Pretty_Tooltip(view, parent, rendering, x, y, body)
+ null
+ }
+ }
graphview.add(panel.peer, BorderLayout.CENTER)
+ graphview.revalidate()
}
- set_graphview(current_graph)
+ set_graphview(current_snapshot, current_graph)
set_content(graphview)
@@ -83,7 +92,7 @@
}
else current_graph
- if (new_graph != current_graph) set_graphview(new_graph)
+ if (new_graph != current_graph) set_graphview(new_snapshot, new_graph)
current_snapshot = new_snapshot
current_state = new_state
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Oct 09 11:51:06 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)
--- a/src/Tools/jEdit/src/rich_text_area.scala Tue Oct 09 00:40:33 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Oct 09 11:51:06 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
}