explict layout graph structure, with dummies and coordinates;
explicit metrics for dummy box;
tuned signature;
misc tuning;

--- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -72,7 +72,7 @@
 
   def apply_layout()
   {
-    visualizer.Coordinates.update_layout()
+    visualizer.update_layout()
     repaint()
   }
 
@@ -80,7 +80,7 @@
   {
     def set_preferred_size()
     {
-      val box = visualizer.Coordinates.bounding_box()
+      val box = visualizer.bounding_box()
       val s = Transform.scale_discrete
 
       preferredSize =
@@ -135,7 +135,7 @@
 
     def apply() =
     {
-      val box = visualizer.Coordinates.bounding_box()
+      val box = visualizer.bounding_box()
       val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
       at.translate(- box.x, - box.y)
       at
@@ -146,7 +146,7 @@
       if (visualizer.visible_graph.is_empty)
         rescale(1.0)
       else {
-        val box = visualizer.Coordinates.bounding_box()
+        val box = visualizer.bounding_box()
         rescale((size.width / box.width) min (size.height / box.height))
       }
     }
@@ -163,7 +163,7 @@
 
   object Mouse_Interaction
   {
-    private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null
+    private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = null
 
     val react: PartialFunction[Event, Unit] =
     {
@@ -175,13 +175,8 @@
       case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
     }
 
-    def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
-      visualizer.visible_graph.edges_iterator.map(edge =>
-        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.
-          collectFirst({
-            case (edge, (d, index))
-            if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index)
-          })
+    def dummy(at: Point2D): Option[Layout.Dummy] =
+      visualizer.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
 
     def pressed(at: Point)
     {
@@ -238,7 +233,7 @@
       }
     }
 
-    def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point)
+    def drag(info: (Point, List[Graph_Display.Node], List[Layout.Dummy]), to: Point)
     {
       val (from, p, d) = info
 
@@ -247,15 +242,14 @@
       (p, d) match {
         case (Nil, Nil) =>
           val r = panel.peer.getViewport.getViewRect
-          r.translate(-dx, -dy)
-
+          r.translate(- dx, - dy)
           paint_panel.peer.scrollRectToVisible(r)
 
         case (Nil, ds) =>
-          ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s))
+          ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s))
 
         case (ls, _) =>
-          ls.foreach(l => visualizer.Coordinates.translate_node(l, dx / s, dy / s))
+          ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s))
       }
     }
   }

--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -19,136 +19,140 @@
 
 object Layout
 {
+  /* graph structure */
+
+  object Vertex
+  {
+    object Ordering extends scala.math.Ordering[Vertex]
+    {
+      def compare(v1: Vertex, v2: Vertex): Int =
+        (v1, v2) match {
+          case (_: Node, _: Dummy) => -1
+          case (_: Dummy, _: Node) => 1
+          case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
+          case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
+            Graph_Display.Node.Ordering.compare(a1, b1) match {
+              case 0 =>
+                Graph_Display.Node.Ordering.compare(a2, b2) match {
+                  case 0 => i compare j
+                  case ord => ord
+                }
+              case ord => ord
+            }
+        }
+    }
+  }
+
+  sealed abstract class Vertex
+  case class Node(node: Graph_Display.Node) extends Vertex
+  case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
+
   object Point { val zero: Point = Point(0.0, 0.0) }
   case class Point(x: Double, y: Double)
 
-  private type Key = Graph_Display.Node
-  private type Coordinates = Map[Key, Point]
-  private type Level = List[Key]
-  private type Levels = List[Level]
+  type Graph = isabelle.Graph[Vertex, Point]
+
+  def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph =
+    isabelle.Graph.make(entries)(Vertex.Ordering)
 
-  val empty: Layout =
-    new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty)
+  val empty_graph: Graph = make_graph(Nil)
+
+
+  /* layout */
+
+  val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
 
   val pendulum_iterations = 10
   val minimize_crossings_iterations = 40
 
-  def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout =
+
+  private type Levels = Map[Vertex, Int]
+  private val empty_levels: Levels = Map.empty
+
+  def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout =
   {
-    if (visible_graph.is_empty) empty
+    if (input_graph.is_empty) empty
     else {
-      val initial_levels = level_map(visible_graph)
+      /* initial graph */
+
+      val initial_graph =
+        make_graph(
+          input_graph.iterator.map(
+            { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList)
 
-      val (dummy_graph, dummies, dummy_levels) =
-        ((visible_graph, Map.empty[(Key, Key), List[Key]], initial_levels) /:
-          visible_graph.edges_iterator) {
-            case ((graph, dummies, levels), (from, to)) =>
-              if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
+      val initial_levels: Levels =
+        (empty_levels /: initial_graph.topological_order) {
+          case (levels, vertex) =>
+            val level =
+              1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
+            levels + (vertex -> level)
+        }
+
+
+      /* graph with dummies */
+
+      val (dummy_graph, dummy_levels) =
+        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
+            case ((graph, levels), (node1, node2)) =>
+              val v1 = Node(node1); val l1 = levels(v1)
+              val v2 = Node(node2); val l2 = levels(v2)
+              if (l2 - l1 <= 1) (graph, levels)
               else {
-                val (graph1, ds, levels1) = add_dummies(graph, from, to, levels)
-                (graph1, dummies + ((from, to) -> ds), levels1)
+                val dummies_levels =
+                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
+                    yield (Dummy(node1, node2, i), l)).toList
+                val dummies = dummies_levels.map(_._1)
+
+                val levels1 = (levels /: dummies_levels)(_ + _)
+                val graph1 =
+                  ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /:
+                    (v1 :: dummies ::: List(v2)).sliding(2)) {
+                      case (g, List(a, b)) => g.add_edge(a, b) }
+                (graph1, levels1)
               }
           }
 
+
+      /* minimize edge crossings and initial coordinates */
+
       val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
 
-      val initial_coordinates: Coordinates =
-        (((Map.empty[Key, Point], 0.0) /: levels) {
-          case ((coords1, y), level) =>
-            ((((coords1, 0.0) /: level) {
-              case ((coords2, x), key) =>
-                val w2 = metrics.box_width2(key)
-                (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
+      val levels_graph: Graph =
+        (((dummy_graph, 0.0) /: levels) {
+          case ((graph, y), level) =>
+            ((((graph, 0.0) /: level) {
+              case ((g, x), v) =>
+                val w2 = metrics.box_width2(v)
+                (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
             })._1, y + metrics.box_height(level.length))
         })._1
 
 
-      val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates)
+      /* pendulum layout */
 
-      val dummy_coords =
-        (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
-          case (map, key) => map + (key -> dummies(key).map(coords(_)))
-        }
+      val output_graph = pendulum(metrics, levels_graph, levels)
 
-      new Layout(metrics, visible_graph, coords, dummy_coords)
+      new Layout(metrics, input_graph, output_graph)
     }
   }
 
 
-  def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int])
-    : (Graph_Display.Graph, List[Key], Map[Key, Int]) =
-  {
-    val ds =
-      ((levels(from) + 1) until levels(to)).map(l => {
-          // FIXME !?
-          val ident = "%s$%s$%d".format(from.ident, to.ident, l)
-          Graph_Display.Node(" ", ident)
-        }).toList
 
-    val ls =
-      (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
-        case (ls, (l, d)) => ls + (d -> l)
-      }
-
-    val graph1 = (graph /: ds)(_.new_node(_, Nil))
-    val graph2 =
-      (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
-        case (g, List(x, y)) => g.add_edge(x, y)
-      }
-    (graph2, ds, ls)
-  }
-
-  def level_map(graph: Graph_Display.Graph): Map[Key, Int] =
-    (Map.empty[Key, Int] /: graph.topological_order) {
-      (levels, key) => {
-        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
-        levels + (key -> lev)
-      }
-    }
+  /** edge crossings **/
 
-  def level_list(map: Map[Key, Int]): Levels =
-  {
-    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(Graph_Display.Node.Ordering)).toList
-  }
+  private type Level = List[Vertex]
 
-  def count_crossings(graph: Graph_Display.Graph, levels: Levels): Int =
-  {
-    def in_level(ls: Levels): Int = ls match {
-      case List(top, bot) =>
-        top.iterator.zipWithIndex.map {
-          case (outer_parent, outer_parent_index) =>
-            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
-            .map(outer_child =>
-              (0 until outer_parent_index)
-              .map(inner_parent =>
-                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
-                .filter(inner_child => outer_child < inner_child)
-                .size
-              ).sum
-            ).sum
-        }.sum
-
-      case _ => 0
-    }
-
-    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
-  }
-
-  def minimize_crossings(graph: Graph_Display.Graph, levels: Levels): Levels =
+  def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
   {
     def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
-      child.map(k => {
-          val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
+      child.map(v => {
+          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
           val weight =
             (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
-          (k, weight)
+          (v, weight)
       }).sortBy(_._2).map(_._1)
 
-    def resort(levels: Levels, top_down: Boolean) =
+    def resort(levels: List[Level], top_down: Boolean) =
       if (top_down)
         (List(levels.head) /: levels.tail)((tops, bot) =>
           resort_level(tops.head, bot, top_down) :: tops).reverse
@@ -170,26 +174,85 @@
     }._1
   }
 
-  def pendulum(
-    metrics: Metrics, graph: Graph_Display.Graph,
-    levels: Levels, coords: Map[Key, Point]): Coordinates =
+  def level_list(levels: Levels): List[Level] =
   {
-    type Regions = List[List[Region]]
+    val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
+    val buckets = new Array[Level](max_lev + 1)
+    for (l <- 0 to max_lev) { buckets(l) = Nil }
+    for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
+    buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
+  }
 
-    def iteration(
-      coords: Coordinates, regions: Regions, top_down: Boolean): (Coordinates, Regions, Boolean) =
-    {
-      val (coords1, regions1, moved) =
-      ((coords, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
-        case ((coords, tops, moved), bot) =>
-          val bot1 = collapse(coords, bot, top_down)
-          val (coords1, moved1) = deflect(coords, bot1, top_down)
-          (coords1, bot1 :: tops, moved || moved1)
-      }
-      (coords1, regions1.reverse, moved)
+  def count_crossings(graph: Graph, levels: List[Level]): Int =
+  {
+    def in_level(ls: List[Level]): Int = ls match {
+      case List(top, bot) =>
+        top.iterator.zipWithIndex.map {
+          case (outer_parent, outer_parent_index) =>
+            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
+            .map(outer_child =>
+              (0 until outer_parent_index)
+              .map(inner_parent =>
+                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
+                .filter(inner_child => outer_child < inner_child)
+                .size
+              ).sum
+            ).sum
+        }.sum
+
+      case _ => 0
     }
 
-    def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] =
+    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
+  }
+
+
+
+  /** pendulum method **/
+
+  /*This is an auxiliary class which is used by the layout algorithm when
+    calculating coordinates with the "pendulum method". A "region" is a
+    group of vertices which "stick together".*/
+  private class Region(init: Vertex)
+  {
+    var content: List[Vertex] = List(init)
+
+    def distance(metrics: Metrics, graph: Graph, that: Region): Double =
+    {
+      val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1)
+      val v2 = that.content.head; val x2 = graph.get_node(v2).x - metrics.box_width2(v2)
+      x2 - x1 - metrics.box_gap
+    }
+
+    def deflection(graph: Graph, top_down: Boolean): Double =
+      ((for (a <- content.iterator) yield {
+        val x = graph.get_node(a).x
+        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
+        bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
+      }).sum / content.length).round.toDouble
+
+    def move(graph: Graph, dx: Double): Graph =
+      if (dx == 0.0) graph
+      else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) }
+  }
+
+  private type Regions = List[List[Region]]
+
+  def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
+  {
+    def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
+    {
+      val (graph1, regions1, moved) =
+      ((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
+        case ((graph, tops, moved), bot) =>
+          val bot1 = collapse(graph, bot, top_down)
+          val (graph1, moved1) = deflect(graph, bot1, top_down)
+          (graph1, bot1 :: tops, moved || moved1)
+      }
+      (graph1, regions1.reverse, moved)
+    }
+
+    def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] =
     {
       if (level.size <= 1) level
       else {
@@ -199,16 +262,16 @@
           regions_changed = false
           for (i <- Range(next.length - 1, 0, -1)) {
             val (r1, r2) = (next(i - 1), next(i))
-            val d1 = r1.deflection(graph, coords, top_down)
-            val d2 = r2.deflection(graph, coords, top_down)
+            val d1 = r1.deflection(graph, top_down)
+            val d2 = r2.deflection(graph, top_down)
 
             if (// Do regions touch?
-                r1.distance(metrics, coords, r2) <= 0.0 &&
+                r1.distance(metrics, graph, r2) <= 0.0 &&
                 // Do they influence each other?
                 (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
             {
               regions_changed = true
-              r1.nodes = r1.nodes ::: r2.nodes
+              r1.content = r1.content ::: r2.content
               next = next.filter(next.indexOf(_) != i)
             }
           }
@@ -217,101 +280,74 @@
       }
     }
 
-    def deflect(
-      coords: Coordinates, level: List[Region], top_down: Boolean): (Coordinates, Boolean) =
+    def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) =
     {
-      ((coords, false) /: (0 until level.length)) {
-        case ((coords, moved), i) =>
+      ((graph, false) /: (0 until level.length)) {
+        case ((graph, moved), i) =>
           val r = level(i)
-          val d = r.deflection(graph, coords, top_down)
+          val d = r.deflection(graph, top_down)
           val offset =
             if (d < 0 && i > 0)
-              - (level(i - 1).distance(metrics, coords, r) min (- d))
+              - (level(i - 1).distance(metrics, graph, r) min (- d))
             else if (d >= 0 && i < level.length - 1)
-              r.distance(metrics, coords, level(i + 1)) min d
+              r.distance(metrics, graph, level(i + 1)) min d
             else d
-          (r.move(coords, offset), moved || d != 0)
+          (r.move(graph, offset), moved || d != 0)
       }
     }
 
-    val regions = levels.map(level => level.map(new Region(_)))
-
-    ((coords, regions, true, true) /: (1 to pendulum_iterations)) {
-      case ((coords, regions, top_down, moved), _) =>
-        if (moved) {
-          val (coords1, regions1, m) = iteration(coords, regions, top_down)
-          (coords1, regions1, !top_down, m)
-        }
-        else (coords, regions, !top_down, moved)
-    }._1
-  }
-
-  /*This is an auxiliary class which is used by the layout algorithm when
-    calculating coordinates with the "pendulum method". A "region" is a
-    group of nodes which "stick together".*/
-  private class Region(node: Key)
-  {
-    var nodes: List[Key] = List(node)
+    val initial_regions = levels.map(level => level.map(new Region(_)))
 
-    def distance(metrics: Metrics, coords: Coordinates, that: Region): Double =
-    {
-      val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1)
-      val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2)
-      x2 - x1 - metrics.box_gap
-    }
-
-    def deflection(graph: Graph_Display.Graph, coords: Coordinates, top_down: Boolean): Double =
-      ((for (a <- nodes.iterator) yield {
-        val x = coords(a).x
-        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
-        bs.iterator.map(coords(_).x - x).sum / (bs.size max 1)
-      }).sum / nodes.length).round.toDouble
-
-    def move(coords: Coordinates, dx: Double): Coordinates =
-      if (dx == 0.0) coords
-      else
-        (coords /: nodes) {
-          case (cs, node) =>
-            val p = cs(node)
-            cs + (node -> Point(p.x + dx, p.y))
+    ((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) {
+      case ((graph, regions, top_down, moved), _) =>
+        if (moved) {
+          val (graph1, regions1, moved1) = iteration(graph, regions, top_down)
+          (graph1, regions1, !top_down, moved1)
         }
+        else (graph, regions, !top_down, moved)
+    }._1
   }
 }
 
 final class Layout private(
   val metrics: Metrics,
-  val visible_graph: Graph_Display.Graph,
-  nodes: Map[Graph_Display.Node, Layout.Point],
-  dummies: Map[Graph_Display.Edge, List[Layout.Point]])
+  val input_graph: Graph_Display.Graph,
+  val output_graph: Layout.Graph)
 {
-  /* nodes */
+  /* vertex coordinates */
+
+  def get_vertex(v: Layout.Vertex): Layout.Point =
+    if (output_graph.defined(v)) output_graph.get_node(v)
+    else Layout.Point.zero
 
-  def get_node(node: Graph_Display.Node): Layout.Point =
-    nodes.getOrElse(node, Layout.Point.zero)
-
-  def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
-    nodes.get(node) match {
-      case None => this
-      case Some(p) =>
-        val nodes1 = nodes + (node -> f(p))
-        new Layout(metrics, visible_graph, nodes1, dummies)
+  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
+  {
+    if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
+    else {
+      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dy, p.y + dy))
+      new Layout(metrics, input_graph, output_graph1)
     }
+  }
 
 
   /* dummies */
 
-  def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
-    dummies.getOrElse(edge, Nil)
-
-  def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
-    dummies.get(edge) match {
-      case None => this
-      case Some(ds) =>
-        val dummies1 = dummies + (edge -> f(ds))
-        new Layout(metrics, visible_graph, nodes, dummies1)
-    }
+  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
+    output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
 
   def dummies_iterator: Iterator[Layout.Point] =
-    for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
+    for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
+
+  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
+    new Iterator[Layout.Point] {
+      private var index = 0
+      def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
+      def next: Layout.Point =
+      {
+        val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
+        index += 1
+        p
+      }
+    }
 }
 

--- a/src/Tools/Graphview/main_panel.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -66,7 +66,7 @@
 
   private def export(file: JFile)
   {
-    val box = visualizer.Coordinates.bounding_box()
+    val box = visualizer.bounding_box()
     val w = box.width.ceil.toInt
     val h = box.height.ceil.toInt
 

--- a/src/Tools/Graphview/metrics.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/metrics.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -38,8 +38,16 @@
   def pad_x: Double = char_width * 1.5
   def pad_y: Double = char_width
 
+  def dummy_width2: Double = (pad_x / 2).ceil
+
   def box_width2(node: Graph_Display.Node): Double =
     ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
+
+  def box_width2(vertex: Layout.Vertex): Double =
+    vertex match {
+      case Layout.Node(node) => box_width2(node)
+      case _: Layout.Dummy => dummy_width2
+    }
   def box_gap: Double = gap.ceil
   def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
 }

--- a/src/Tools/Graphview/shapes.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -24,11 +24,11 @@
     def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
     {
       val metrics = visualizer.metrics
-      val p = visualizer.Coordinates.get_node(node)
+      val p = visualizer.get_vertex(Layout.Node(node))
       val bounds = metrics.string_bounds(node.toString)
-      val w = bounds.getWidth + metrics.pad_x
-      val h = bounds.getHeight + metrics.pad_y
-      new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
+      val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil
+      val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil
+      new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2)
     }
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
@@ -58,8 +58,8 @@
     def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
     {
       val metrics = visualizer.metrics
-      val w = metrics.pad_x
-      new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
+      val w = metrics.dummy_width2
+      new Rectangle2D.Double(d.x - w / 2, d.y - w / 2, w, w)
     }
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
@@ -74,13 +74,13 @@
   {
     def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
-      val p = visualizer.Coordinates.get_node(edge._1)
-      val q = visualizer.Coordinates.get_node(edge._2)
+      val p = visualizer.get_vertex(Layout.Node(edge._1))
+      val q = visualizer.get_vertex(Layout.Node(edge._2))
       val ds =
       {
         val a = p.y min q.y
         val b = p.y max q.y
-        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
+        visualizer.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.Coordinates.get_node(edge._1)
-      val q = visualizer.Coordinates.get_node(edge._2)
+      val p = visualizer.get_vertex(Layout.Node(edge._1))
+      val q = visualizer.get_vertex(Layout.Node(edge._2))
       val ds =
       {
         val a = p.y min q.y
         val b = p.y max q.y
-        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
+        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
       }
 
       if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)

--- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:33:30 2015 +0100
@@ -19,11 +19,57 @@
 {
   visualizer =>
 
+
+  /* layout state */
+
   // owned by GUI thread
   private var layout: Layout = Layout.empty
 
   def metrics: Metrics = layout.metrics
-  def visible_graph: Graph_Display.Graph = layout.visible_graph
+  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 bounding_box(): Rectangle2D.Double =
+  {
+    var x0 = 0.0
+    var y0 = 0.0
+    var x1 = 0.0
+    var y1 = 0.0
+    ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
+     (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
+       foreach(rect => {
+          x0 = x0 min rect.getMinX
+          y0 = y0 min rect.getMinY
+          x1 = x1 max rect.getMaxX
+          y1 = y1 max rect.getMaxY
+        })
+    val gap = metrics.gap
+    x0 = (x0 - gap).floor
+    y0 = (y0 - gap).floor
+    x1 = (x1 + gap).ceil
+    y1 = (y1 + gap).ceil
+    new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
+  }
+
+  def update_layout()
+  {
+    val metrics = Metrics(make_font())
+    val visible_graph = model.make_visible_graph()
+
+    // FIXME avoid expensive operation on GUI thread
+    layout = Layout.make(metrics, visible_graph)
+  }
 
 
   /* tooltips */
@@ -85,60 +131,6 @@
       Shapes.Node.paint(gfx, visualizer, node)
   }
 
-  object Coordinates
-  {
-    def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node)
-    def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge)
-
-    def translate_node(node: Graph_Display.Node, dx: Double, dy: Double)
-    {
-      layout = layout.map_node(node, p => Layout.Point(p.x + dx, p.y + dy))
-    }
-
-    def translate_dummy(d: (Graph_Display.Edge, Int), dx: Double, dy: Double)
-    {
-      val (edge, index) = d
-      layout = layout.map_dummies(edge,
-        ds => {
-          val p = ds(index)
-          (ds.zipWithIndex :\ List.empty[Layout.Point]) {
-            case ((t, i), n) => if (index == i) Layout.Point(p.x + dx, p.y + dy) :: n else t :: n
-          }
-        })
-    }
-
-    def update_layout()
-    {
-      val metrics = Metrics(make_font())
-      val visible_graph = model.make_visible_graph()
-
-      // FIXME avoid expensive operation on GUI thread
-      layout = Layout.make(metrics, visible_graph)
-    }
-
-    def bounding_box(): Rectangle2D.Double =
-    {
-      var x0 = 0.0
-      var y0 = 0.0
-      var x1 = 0.0
-      var y1 = 0.0
-      ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
-       (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
-         foreach(rect => {
-            x0 = x0 min rect.getMinX
-            y0 = y0 min rect.getMinY
-            x1 = x1 max rect.getMaxX
-            y1 = y1 max rect.getMaxY
-          })
-      val gap = metrics.gap
-      x0 = (x0 - gap).floor
-      y0 = (y0 - gap).floor
-      x1 = (x1 + gap).ceil
-      y1 = (y1 + gap).ceil
-      new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
-    }
-  }
-
   object Selection
   {
     // owned by GUI thread