src/Tools/Graphview/graph_panel.scala

 package isabelle.graphview
 
 
 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}
 
 import scala.swing.{Panel, ScrollPane}
 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}

   visualizer.model.Colors.events += { case _ => repaint() }
   visualizer.model.Mutators.events += { case _ => repaint() }
 
   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
     def scale: Double = _scale
     def scale_=(s: Double)

     }
 
     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()
     {
       if (visualizer.visible_graph.is_empty)