# HG changeset patch # User wenzelm # Date 1421613354 -3600 # Node ID fc909f7e7ce51798937c442ea0db902beb229aed # Parent a2f4252c5489126ee62e333d6e160c6239c6e9ac proper scrolling wrt. transform; tuned signature; diff -r a2f4252c5489 -r fc909f7e7ce5 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Sun Jan 18 20:15:05 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 18 21:35:54 2015 +0100 @@ -10,7 +10,7 @@ import isabelle._ -import java.awt.{Dimension, Graphics2D, Point} +import java.awt.{Dimension, Graphics2D, Point, Rectangle} import java.awt.geom.{AffineTransform, Point2D} import javax.swing.{JScrollPane, JComponent, SwingUtilities} @@ -105,6 +105,24 @@ rescale(1.0) + + def scroll_to_node(node: Graph_Display.Node) + { + val gap = visualizer.metrics.gap + val info = visualizer.layout.get_node(node) + + val t = Transform() + val p = + t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null) + val q = + t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null) + + paint_panel.peer.scrollRectToVisible( + new Rectangle(p.getX.toInt, p.getY.toInt, + (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt)) + } + + private object Transform { private var _scale: Double = 1.0 @@ -123,9 +141,9 @@ def apply() = { val box = visualizer.bounding_box() - val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) - at.translate(- box.x, - box.y) - at + val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) + t.translate(- box.x, - box.y) + t } def fit_to_window() diff -r a2f4252c5489 -r fc909f7e7ce5 src/Tools/Graphview/main_panel.scala --- a/src/Tools/Graphview/main_panel.scala Sun Jan 18 20:15:05 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Sun Jan 18 21:35:54 2015 +0100 @@ -21,14 +21,8 @@ class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel { - private def repaint_all() - { - revalidate() - repaint() - } - val graph_panel = new Graph_Panel(visualizer) - val tree_panel = new Tree_Panel(visualizer, repaint_all _) + val tree_panel = new Tree_Panel(visualizer, graph_panel) def update_layout() { diff -r a2f4252c5489 -r fc909f7e7ce5 src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Sun Jan 18 20:15:05 2015 +0100 +++ b/src/Tools/Graphview/tree_panel.scala Sun Jan 18 21:35:54 2015 +0100 @@ -19,7 +19,7 @@ import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action} -class Tree_Panel(val visualizer: Visualizer, repaint_all: () => Unit) extends BorderPanel +class Tree_Panel(val visualizer: Visualizer, graph_panel: Graph_Panel) extends BorderPanel { /* main actions */ @@ -41,7 +41,7 @@ } } } - repaint_all() + graph_panel.repaint() } } @@ -57,17 +57,9 @@ } case _ => None } - action_node match { - case Some(node) => - val info = visualizer.layout.get_node(node) - tree_pane.peer.scrollRectToVisible( - new Rectangle( - (info.x - info.width2).toInt, (info.y - info.height2).toInt, - info.width.toInt, info.height.toInt)) - case None => - } + action_node.foreach(graph_panel.scroll_to_node(_)) visualizer.current_node = action_node - repaint_all() + graph_panel.repaint() } }