# HG changeset patch
# User wenzelm
# Date 1420558891 -3600
# Node ID 15cd9bcd6ddbf5e488f7379113c7d7bb5d559398
# Parent  4d985afc05656d1c866f88cfba046de969604db2
tuned signature;

diff -r 4d985afc0565 -r 15cd9bcd6ddb src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:33:30 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:41:31 2015 +0100
@@ -176,7 +176,7 @@
     }
 
     def dummy(at: Point2D): Option[Layout.Dummy] =
-      visualizer.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
+      visualizer.layout.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
 
     def pressed(at: Point)
     {
diff -r 4d985afc0565 -r 15cd9bcd6ddb src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:33:30 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:41:31 2015 +0100
@@ -24,7 +24,7 @@
     def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
     {
       val metrics = visualizer.metrics
-      val p = visualizer.get_vertex(Layout.Node(node))
+      val p = visualizer.layout.get_vertex(Layout.Node(node))
       val bounds = metrics.string_bounds(node.toString)
       val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil
       val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil
@@ -74,13 +74,13 @@
   {
     def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
-      val p = visualizer.get_vertex(Layout.Node(edge._1))
-      val q = visualizer.get_vertex(Layout.Node(edge._2))
+      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
+      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
       val ds =
       {
         val a = p.y min q.y
         val b = p.y max q.y
-        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
+        visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
       }
       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
 
@@ -106,13 +106,13 @@
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
-      val p = visualizer.get_vertex(Layout.Node(edge._1))
-      val q = visualizer.get_vertex(Layout.Node(edge._2))
+      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
+      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
       val ds =
       {
         val a = p.y min q.y
         val b = p.y max q.y
-        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
+        visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
       }
 
       if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
diff -r 4d985afc0565 -r 15cd9bcd6ddb src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:33:30 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:41:31 2015 +0100
@@ -23,22 +23,14 @@
   /* layout state */
 
   // owned by GUI thread
-  private var layout: Layout = Layout.empty
+  private var _layout: Layout = Layout.empty
+  def layout: Layout = _layout
 
   def metrics: Metrics = layout.metrics
   def visible_graph: Graph_Display.Graph = layout.input_graph
 
-  def get_vertex(v: Layout.Vertex): Layout.Point = layout.get_vertex(v)
-  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double)
-  {
-    layout = layout.translate_vertex(v, dx, dy)
-  }
-
-  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
-    layout.dummies_iterator(edge)
-
-  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
-    layout.find_dummy(pred)
+  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
+    _layout = _layout.translate_vertex(v, dx, dy)
 
   def bounding_box(): Rectangle2D.Double =
   {
@@ -68,7 +60,7 @@
     val visible_graph = model.make_visible_graph()
 
     // FIXME avoid expensive operation on GUI thread
-    layout = Layout.make(metrics, visible_graph)
+    _layout = Layout.make(metrics, visible_graph)
   }