# 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()
     }
   }