explict layout graph structure, with dummies and coordinates;
authorwenzelm
Tue Jan 06 16:33:30 2015 +0100 (2015-01-06)
changeset 593024d985afc0565
parent 59301 9089639ba348
child 59303 15cd9bcd6ddb
explict layout graph structure, with dummies and coordinates;
explicit metrics for dummy box;
tuned signature;
misc tuning;
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/layout.scala
src/Tools/Graphview/main_panel.scala
src/Tools/Graphview/metrics.scala
src/Tools/Graphview/shapes.scala
src/Tools/Graphview/visualizer.scala
     1.1 --- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 11:58:57 2015 +0100
     1.2 +++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:33:30 2015 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5    def apply_layout()
     1.6    {
     1.7 -    visualizer.Coordinates.update_layout()
     1.8 +    visualizer.update_layout()
     1.9      repaint()
    1.10    }
    1.11  
    1.12 @@ -80,7 +80,7 @@
    1.13    {
    1.14      def set_preferred_size()
    1.15      {
    1.16 -      val box = visualizer.Coordinates.bounding_box()
    1.17 +      val box = visualizer.bounding_box()
    1.18        val s = Transform.scale_discrete
    1.19  
    1.20        preferredSize =
    1.21 @@ -135,7 +135,7 @@
    1.22  
    1.23      def apply() =
    1.24      {
    1.25 -      val box = visualizer.Coordinates.bounding_box()
    1.26 +      val box = visualizer.bounding_box()
    1.27        val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
    1.28        at.translate(- box.x, - box.y)
    1.29        at
    1.30 @@ -146,7 +146,7 @@
    1.31        if (visualizer.visible_graph.is_empty)
    1.32          rescale(1.0)
    1.33        else {
    1.34 -        val box = visualizer.Coordinates.bounding_box()
    1.35 +        val box = visualizer.bounding_box()
    1.36          rescale((size.width / box.width) min (size.height / box.height))
    1.37        }
    1.38      }
    1.39 @@ -163,7 +163,7 @@
    1.40  
    1.41    object Mouse_Interaction
    1.42    {
    1.43 -    private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null
    1.44 +    private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = null
    1.45  
    1.46      val react: PartialFunction[Event, Unit] =
    1.47      {
    1.48 @@ -175,13 +175,8 @@
    1.49        case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
    1.50      }
    1.51  
    1.52 -    def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
    1.53 -      visualizer.visible_graph.edges_iterator.map(edge =>
    1.54 -        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.
    1.55 -          collectFirst({
    1.56 -            case (edge, (d, index))
    1.57 -            if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index)
    1.58 -          })
    1.59 +    def dummy(at: Point2D): Option[Layout.Dummy] =
    1.60 +      visualizer.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
    1.61  
    1.62      def pressed(at: Point)
    1.63      {
    1.64 @@ -238,7 +233,7 @@
    1.65        }
    1.66      }
    1.67  
    1.68 -    def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point)
    1.69 +    def drag(info: (Point, List[Graph_Display.Node], List[Layout.Dummy]), to: Point)
    1.70      {
    1.71        val (from, p, d) = info
    1.72  
    1.73 @@ -247,15 +242,14 @@
    1.74        (p, d) match {
    1.75          case (Nil, Nil) =>
    1.76            val r = panel.peer.getViewport.getViewRect
    1.77 -          r.translate(-dx, -dy)
    1.78 -
    1.79 +          r.translate(- dx, - dy)
    1.80            paint_panel.peer.scrollRectToVisible(r)
    1.81  
    1.82          case (Nil, ds) =>
    1.83 -          ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s))
    1.84 +          ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s))
    1.85  
    1.86          case (ls, _) =>
    1.87 -          ls.foreach(l => visualizer.Coordinates.translate_node(l, dx / s, dy / s))
    1.88 +          ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s))
    1.89        }
    1.90      }
    1.91    }
     2.1 --- a/src/Tools/Graphview/layout.scala	Tue Jan 06 11:58:57 2015 +0100
     2.2 +++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 16:33:30 2015 +0100
     2.3 @@ -19,136 +19,140 @@
     2.4  
     2.5  object Layout
     2.6  {
     2.7 +  /* graph structure */
     2.8 +
     2.9 +  object Vertex
    2.10 +  {
    2.11 +    object Ordering extends scala.math.Ordering[Vertex]
    2.12 +    {
    2.13 +      def compare(v1: Vertex, v2: Vertex): Int =
    2.14 +        (v1, v2) match {
    2.15 +          case (_: Node, _: Dummy) => -1
    2.16 +          case (_: Dummy, _: Node) => 1
    2.17 +          case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
    2.18 +          case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
    2.19 +            Graph_Display.Node.Ordering.compare(a1, b1) match {
    2.20 +              case 0 =>
    2.21 +                Graph_Display.Node.Ordering.compare(a2, b2) match {
    2.22 +                  case 0 => i compare j
    2.23 +                  case ord => ord
    2.24 +                }
    2.25 +              case ord => ord
    2.26 +            }
    2.27 +        }
    2.28 +    }
    2.29 +  }
    2.30 +
    2.31 +  sealed abstract class Vertex
    2.32 +  case class Node(node: Graph_Display.Node) extends Vertex
    2.33 +  case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
    2.34 +
    2.35    object Point { val zero: Point = Point(0.0, 0.0) }
    2.36    case class Point(x: Double, y: Double)
    2.37  
    2.38 -  private type Key = Graph_Display.Node
    2.39 -  private type Coordinates = Map[Key, Point]
    2.40 -  private type Level = List[Key]
    2.41 -  private type Levels = List[Level]
    2.42 +  type Graph = isabelle.Graph[Vertex, Point]
    2.43  
    2.44 -  val empty: Layout =
    2.45 -    new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty)
    2.46 +  def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph =
    2.47 +    isabelle.Graph.make(entries)(Vertex.Ordering)
    2.48 +
    2.49 +  val empty_graph: Graph = make_graph(Nil)
    2.50 +
    2.51 +
    2.52 +  /* layout */
    2.53 +
    2.54 +  val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
    2.55  
    2.56    val pendulum_iterations = 10
    2.57    val minimize_crossings_iterations = 40
    2.58  
    2.59 -  def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout =
    2.60 +
    2.61 +  private type Levels = Map[Vertex, Int]
    2.62 +  private val empty_levels: Levels = Map.empty
    2.63 +
    2.64 +  def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout =
    2.65    {
    2.66 -    if (visible_graph.is_empty) empty
    2.67 +    if (input_graph.is_empty) empty
    2.68      else {
    2.69 -      val initial_levels = level_map(visible_graph)
    2.70 +      /* initial graph */
    2.71  
    2.72 -      val (dummy_graph, dummies, dummy_levels) =
    2.73 -        ((visible_graph, Map.empty[(Key, Key), List[Key]], initial_levels) /:
    2.74 -          visible_graph.edges_iterator) {
    2.75 -            case ((graph, dummies, levels), (from, to)) =>
    2.76 -              if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
    2.77 +      val initial_graph =
    2.78 +        make_graph(
    2.79 +          input_graph.iterator.map(
    2.80 +            { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList)
    2.81 +
    2.82 +      val initial_levels: Levels =
    2.83 +        (empty_levels /: initial_graph.topological_order) {
    2.84 +          case (levels, vertex) =>
    2.85 +            val level =
    2.86 +              1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
    2.87 +            levels + (vertex -> level)
    2.88 +        }
    2.89 +
    2.90 +
    2.91 +      /* graph with dummies */
    2.92 +
    2.93 +      val (dummy_graph, dummy_levels) =
    2.94 +        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
    2.95 +            case ((graph, levels), (node1, node2)) =>
    2.96 +              val v1 = Node(node1); val l1 = levels(v1)
    2.97 +              val v2 = Node(node2); val l2 = levels(v2)
    2.98 +              if (l2 - l1 <= 1) (graph, levels)
    2.99                else {
   2.100 -                val (graph1, ds, levels1) = add_dummies(graph, from, to, levels)
   2.101 -                (graph1, dummies + ((from, to) -> ds), levels1)
   2.102 +                val dummies_levels =
   2.103 +                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
   2.104 +                    yield (Dummy(node1, node2, i), l)).toList
   2.105 +                val dummies = dummies_levels.map(_._1)
   2.106 +
   2.107 +                val levels1 = (levels /: dummies_levels)(_ + _)
   2.108 +                val graph1 =
   2.109 +                  ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /:
   2.110 +                    (v1 :: dummies ::: List(v2)).sliding(2)) {
   2.111 +                      case (g, List(a, b)) => g.add_edge(a, b) }
   2.112 +                (graph1, levels1)
   2.113                }
   2.114            }
   2.115  
   2.116 +
   2.117 +      /* minimize edge crossings and initial coordinates */
   2.118 +
   2.119        val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
   2.120  
   2.121 -      val initial_coordinates: Coordinates =
   2.122 -        (((Map.empty[Key, Point], 0.0) /: levels) {
   2.123 -          case ((coords1, y), level) =>
   2.124 -            ((((coords1, 0.0) /: level) {
   2.125 -              case ((coords2, x), key) =>
   2.126 -                val w2 = metrics.box_width2(key)
   2.127 -                (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
   2.128 +      val levels_graph: Graph =
   2.129 +        (((dummy_graph, 0.0) /: levels) {
   2.130 +          case ((graph, y), level) =>
   2.131 +            ((((graph, 0.0) /: level) {
   2.132 +              case ((g, x), v) =>
   2.133 +                val w2 = metrics.box_width2(v)
   2.134 +                (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
   2.135              })._1, y + metrics.box_height(level.length))
   2.136          })._1
   2.137  
   2.138  
   2.139 -      val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates)
   2.140 +      /* pendulum layout */
   2.141  
   2.142 -      val dummy_coords =
   2.143 -        (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
   2.144 -          case (map, key) => map + (key -> dummies(key).map(coords(_)))
   2.145 -        }
   2.146 +      val output_graph = pendulum(metrics, levels_graph, levels)
   2.147  
   2.148 -      new Layout(metrics, visible_graph, coords, dummy_coords)
   2.149 +      new Layout(metrics, input_graph, output_graph)
   2.150      }
   2.151    }
   2.152  
   2.153  
   2.154 -  def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int])
   2.155 -    : (Graph_Display.Graph, List[Key], Map[Key, Int]) =
   2.156 -  {
   2.157 -    val ds =
   2.158 -      ((levels(from) + 1) until levels(to)).map(l => {
   2.159 -          // FIXME !?
   2.160 -          val ident = "%s$%s$%d".format(from.ident, to.ident, l)
   2.161 -          Graph_Display.Node(" ", ident)
   2.162 -        }).toList
   2.163  
   2.164 -    val ls =
   2.165 -      (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
   2.166 -        case (ls, (l, d)) => ls + (d -> l)
   2.167 -      }
   2.168 +  /** edge crossings **/
   2.169  
   2.170 -    val graph1 = (graph /: ds)(_.new_node(_, Nil))
   2.171 -    val graph2 =
   2.172 -      (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
   2.173 -        case (g, List(x, y)) => g.add_edge(x, y)
   2.174 -      }
   2.175 -    (graph2, ds, ls)
   2.176 -  }
   2.177 +  private type Level = List[Vertex]
   2.178  
   2.179 -  def level_map(graph: Graph_Display.Graph): Map[Key, Int] =
   2.180 -    (Map.empty[Key, Int] /: graph.topological_order) {
   2.181 -      (levels, key) => {
   2.182 -        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
   2.183 -        levels + (key -> lev)
   2.184 -      }
   2.185 -    }
   2.186 -
   2.187 -  def level_list(map: Map[Key, Int]): Levels =
   2.188 -  {
   2.189 -    val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
   2.190 -    val buckets = new Array[Level](max_lev + 1)
   2.191 -    for (l <- 0 to max_lev) { buckets(l) = Nil }
   2.192 -    for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
   2.193 -    buckets.iterator.map(_.sorted(Graph_Display.Node.Ordering)).toList
   2.194 -  }
   2.195 -
   2.196 -  def count_crossings(graph: Graph_Display.Graph, levels: Levels): Int =
   2.197 -  {
   2.198 -    def in_level(ls: Levels): Int = ls match {
   2.199 -      case List(top, bot) =>
   2.200 -        top.iterator.zipWithIndex.map {
   2.201 -          case (outer_parent, outer_parent_index) =>
   2.202 -            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
   2.203 -            .map(outer_child =>
   2.204 -              (0 until outer_parent_index)
   2.205 -              .map(inner_parent =>
   2.206 -                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
   2.207 -                .filter(inner_child => outer_child < inner_child)
   2.208 -                .size
   2.209 -              ).sum
   2.210 -            ).sum
   2.211 -        }.sum
   2.212 -
   2.213 -      case _ => 0
   2.214 -    }
   2.215 -
   2.216 -    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
   2.217 -  }
   2.218 -
   2.219 -  def minimize_crossings(graph: Graph_Display.Graph, levels: Levels): Levels =
   2.220 +  def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
   2.221    {
   2.222      def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
   2.223 -      child.map(k => {
   2.224 -          val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
   2.225 +      child.map(v => {
   2.226 +          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
   2.227            val weight =
   2.228              (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
   2.229 -          (k, weight)
   2.230 +          (v, weight)
   2.231        }).sortBy(_._2).map(_._1)
   2.232  
   2.233 -    def resort(levels: Levels, top_down: Boolean) =
   2.234 +    def resort(levels: List[Level], top_down: Boolean) =
   2.235        if (top_down)
   2.236          (List(levels.head) /: levels.tail)((tops, bot) =>
   2.237            resort_level(tops.head, bot, top_down) :: tops).reverse
   2.238 @@ -170,26 +174,85 @@
   2.239      }._1
   2.240    }
   2.241  
   2.242 -  def pendulum(
   2.243 -    metrics: Metrics, graph: Graph_Display.Graph,
   2.244 -    levels: Levels, coords: Map[Key, Point]): Coordinates =
   2.245 +  def level_list(levels: Levels): List[Level] =
   2.246    {
   2.247 -    type Regions = List[List[Region]]
   2.248 +    val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
   2.249 +    val buckets = new Array[Level](max_lev + 1)
   2.250 +    for (l <- 0 to max_lev) { buckets(l) = Nil }
   2.251 +    for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
   2.252 +    buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
   2.253 +  }
   2.254  
   2.255 -    def iteration(
   2.256 -      coords: Coordinates, regions: Regions, top_down: Boolean): (Coordinates, Regions, Boolean) =
   2.257 -    {
   2.258 -      val (coords1, regions1, moved) =
   2.259 -      ((coords, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
   2.260 -        case ((coords, tops, moved), bot) =>
   2.261 -          val bot1 = collapse(coords, bot, top_down)
   2.262 -          val (coords1, moved1) = deflect(coords, bot1, top_down)
   2.263 -          (coords1, bot1 :: tops, moved || moved1)
   2.264 -      }
   2.265 -      (coords1, regions1.reverse, moved)
   2.266 +  def count_crossings(graph: Graph, levels: List[Level]): Int =
   2.267 +  {
   2.268 +    def in_level(ls: List[Level]): Int = ls match {
   2.269 +      case List(top, bot) =>
   2.270 +        top.iterator.zipWithIndex.map {
   2.271 +          case (outer_parent, outer_parent_index) =>
   2.272 +            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
   2.273 +            .map(outer_child =>
   2.274 +              (0 until outer_parent_index)
   2.275 +              .map(inner_parent =>
   2.276 +                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
   2.277 +                .filter(inner_child => outer_child < inner_child)
   2.278 +                .size
   2.279 +              ).sum
   2.280 +            ).sum
   2.281 +        }.sum
   2.282 +
   2.283 +      case _ => 0
   2.284      }
   2.285  
   2.286 -    def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] =
   2.287 +    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
   2.288 +  }
   2.289 +
   2.290 +
   2.291 +
   2.292 +  /** pendulum method **/
   2.293 +
   2.294 +  /*This is an auxiliary class which is used by the layout algorithm when
   2.295 +    calculating coordinates with the "pendulum method". A "region" is a
   2.296 +    group of vertices which "stick together".*/
   2.297 +  private class Region(init: Vertex)
   2.298 +  {
   2.299 +    var content: List[Vertex] = List(init)
   2.300 +
   2.301 +    def distance(metrics: Metrics, graph: Graph, that: Region): Double =
   2.302 +    {
   2.303 +      val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1)
   2.304 +      val v2 = that.content.head; val x2 = graph.get_node(v2).x - metrics.box_width2(v2)
   2.305 +      x2 - x1 - metrics.box_gap
   2.306 +    }
   2.307 +
   2.308 +    def deflection(graph: Graph, top_down: Boolean): Double =
   2.309 +      ((for (a <- content.iterator) yield {
   2.310 +        val x = graph.get_node(a).x
   2.311 +        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
   2.312 +        bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
   2.313 +      }).sum / content.length).round.toDouble
   2.314 +
   2.315 +    def move(graph: Graph, dx: Double): Graph =
   2.316 +      if (dx == 0.0) graph
   2.317 +      else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) }
   2.318 +  }
   2.319 +
   2.320 +  private type Regions = List[List[Region]]
   2.321 +
   2.322 +  def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
   2.323 +  {
   2.324 +    def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
   2.325 +    {
   2.326 +      val (graph1, regions1, moved) =
   2.327 +      ((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
   2.328 +        case ((graph, tops, moved), bot) =>
   2.329 +          val bot1 = collapse(graph, bot, top_down)
   2.330 +          val (graph1, moved1) = deflect(graph, bot1, top_down)
   2.331 +          (graph1, bot1 :: tops, moved || moved1)
   2.332 +      }
   2.333 +      (graph1, regions1.reverse, moved)
   2.334 +    }
   2.335 +
   2.336 +    def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] =
   2.337      {
   2.338        if (level.size <= 1) level
   2.339        else {
   2.340 @@ -199,16 +262,16 @@
   2.341            regions_changed = false
   2.342            for (i <- Range(next.length - 1, 0, -1)) {
   2.343              val (r1, r2) = (next(i - 1), next(i))
   2.344 -            val d1 = r1.deflection(graph, coords, top_down)
   2.345 -            val d2 = r2.deflection(graph, coords, top_down)
   2.346 +            val d1 = r1.deflection(graph, top_down)
   2.347 +            val d2 = r2.deflection(graph, top_down)
   2.348  
   2.349              if (// Do regions touch?
   2.350 -                r1.distance(metrics, coords, r2) <= 0.0 &&
   2.351 +                r1.distance(metrics, graph, r2) <= 0.0 &&
   2.352                  // Do they influence each other?
   2.353                  (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
   2.354              {
   2.355                regions_changed = true
   2.356 -              r1.nodes = r1.nodes ::: r2.nodes
   2.357 +              r1.content = r1.content ::: r2.content
   2.358                next = next.filter(next.indexOf(_) != i)
   2.359              }
   2.360            }
   2.361 @@ -217,101 +280,74 @@
   2.362        }
   2.363      }
   2.364  
   2.365 -    def deflect(
   2.366 -      coords: Coordinates, level: List[Region], top_down: Boolean): (Coordinates, Boolean) =
   2.367 +    def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) =
   2.368      {
   2.369 -      ((coords, false) /: (0 until level.length)) {
   2.370 -        case ((coords, moved), i) =>
   2.371 +      ((graph, false) /: (0 until level.length)) {
   2.372 +        case ((graph, moved), i) =>
   2.373            val r = level(i)
   2.374 -          val d = r.deflection(graph, coords, top_down)
   2.375 +          val d = r.deflection(graph, top_down)
   2.376            val offset =
   2.377              if (d < 0 && i > 0)
   2.378 -              - (level(i - 1).distance(metrics, coords, r) min (- d))
   2.379 +              - (level(i - 1).distance(metrics, graph, r) min (- d))
   2.380              else if (d >= 0 && i < level.length - 1)
   2.381 -              r.distance(metrics, coords, level(i + 1)) min d
   2.382 +              r.distance(metrics, graph, level(i + 1)) min d
   2.383              else d
   2.384 -          (r.move(coords, offset), moved || d != 0)
   2.385 +          (r.move(graph, offset), moved || d != 0)
   2.386        }
   2.387      }
   2.388  
   2.389 -    val regions = levels.map(level => level.map(new Region(_)))
   2.390 +    val initial_regions = levels.map(level => level.map(new Region(_)))
   2.391  
   2.392 -    ((coords, regions, true, true) /: (1 to pendulum_iterations)) {
   2.393 -      case ((coords, regions, top_down, moved), _) =>
   2.394 +    ((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) {
   2.395 +      case ((graph, regions, top_down, moved), _) =>
   2.396          if (moved) {
   2.397 -          val (coords1, regions1, m) = iteration(coords, regions, top_down)
   2.398 -          (coords1, regions1, !top_down, m)
   2.399 +          val (graph1, regions1, moved1) = iteration(graph, regions, top_down)
   2.400 +          (graph1, regions1, !top_down, moved1)
   2.401          }
   2.402 -        else (coords, regions, !top_down, moved)
   2.403 +        else (graph, regions, !top_down, moved)
   2.404      }._1
   2.405    }
   2.406 -
   2.407 -  /*This is an auxiliary class which is used by the layout algorithm when
   2.408 -    calculating coordinates with the "pendulum method". A "region" is a
   2.409 -    group of nodes which "stick together".*/
   2.410 -  private class Region(node: Key)
   2.411 -  {
   2.412 -    var nodes: List[Key] = List(node)
   2.413 -
   2.414 -    def distance(metrics: Metrics, coords: Coordinates, that: Region): Double =
   2.415 -    {
   2.416 -      val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1)
   2.417 -      val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2)
   2.418 -      x2 - x1 - metrics.box_gap
   2.419 -    }
   2.420 -
   2.421 -    def deflection(graph: Graph_Display.Graph, coords: Coordinates, top_down: Boolean): Double =
   2.422 -      ((for (a <- nodes.iterator) yield {
   2.423 -        val x = coords(a).x
   2.424 -        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
   2.425 -        bs.iterator.map(coords(_).x - x).sum / (bs.size max 1)
   2.426 -      }).sum / nodes.length).round.toDouble
   2.427 -
   2.428 -    def move(coords: Coordinates, dx: Double): Coordinates =
   2.429 -      if (dx == 0.0) coords
   2.430 -      else
   2.431 -        (coords /: nodes) {
   2.432 -          case (cs, node) =>
   2.433 -            val p = cs(node)
   2.434 -            cs + (node -> Point(p.x + dx, p.y))
   2.435 -        }
   2.436 -  }
   2.437  }
   2.438  
   2.439  final class Layout private(
   2.440    val metrics: Metrics,
   2.441 -  val visible_graph: Graph_Display.Graph,
   2.442 -  nodes: Map[Graph_Display.Node, Layout.Point],
   2.443 -  dummies: Map[Graph_Display.Edge, List[Layout.Point]])
   2.444 +  val input_graph: Graph_Display.Graph,
   2.445 +  val output_graph: Layout.Graph)
   2.446  {
   2.447 -  /* nodes */
   2.448 +  /* vertex coordinates */
   2.449  
   2.450 -  def get_node(node: Graph_Display.Node): Layout.Point =
   2.451 -    nodes.getOrElse(node, Layout.Point.zero)
   2.452 +  def get_vertex(v: Layout.Vertex): Layout.Point =
   2.453 +    if (output_graph.defined(v)) output_graph.get_node(v)
   2.454 +    else Layout.Point.zero
   2.455  
   2.456 -  def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
   2.457 -    nodes.get(node) match {
   2.458 -      case None => this
   2.459 -      case Some(p) =>
   2.460 -        val nodes1 = nodes + (node -> f(p))
   2.461 -        new Layout(metrics, visible_graph, nodes1, dummies)
   2.462 +  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
   2.463 +  {
   2.464 +    if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
   2.465 +    else {
   2.466 +      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dy, p.y + dy))
   2.467 +      new Layout(metrics, input_graph, output_graph1)
   2.468      }
   2.469 +  }
   2.470  
   2.471  
   2.472    /* dummies */
   2.473  
   2.474 -  def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
   2.475 -    dummies.getOrElse(edge, Nil)
   2.476 -
   2.477 -  def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
   2.478 -    dummies.get(edge) match {
   2.479 -      case None => this
   2.480 -      case Some(ds) =>
   2.481 -        val dummies1 = dummies + (edge -> f(ds))
   2.482 -        new Layout(metrics, visible_graph, nodes, dummies1)
   2.483 -    }
   2.484 +  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
   2.485 +    output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
   2.486  
   2.487    def dummies_iterator: Iterator[Layout.Point] =
   2.488 -    for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
   2.489 +    for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
   2.490 +
   2.491 +  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
   2.492 +    new Iterator[Layout.Point] {
   2.493 +      private var index = 0
   2.494 +      def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
   2.495 +      def next: Layout.Point =
   2.496 +      {
   2.497 +        val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
   2.498 +        index += 1
   2.499 +        p
   2.500 +      }
   2.501 +    }
   2.502  }
   2.503  
     3.1 --- a/src/Tools/Graphview/main_panel.scala	Tue Jan 06 11:58:57 2015 +0100
     3.2 +++ b/src/Tools/Graphview/main_panel.scala	Tue Jan 06 16:33:30 2015 +0100
     3.3 @@ -66,7 +66,7 @@
     3.4  
     3.5    private def export(file: JFile)
     3.6    {
     3.7 -    val box = visualizer.Coordinates.bounding_box()
     3.8 +    val box = visualizer.bounding_box()
     3.9      val w = box.width.ceil.toInt
    3.10      val h = box.height.ceil.toInt
    3.11  
     4.1 --- a/src/Tools/Graphview/metrics.scala	Tue Jan 06 11:58:57 2015 +0100
     4.2 +++ b/src/Tools/Graphview/metrics.scala	Tue Jan 06 16:33:30 2015 +0100
     4.3 @@ -38,8 +38,16 @@
     4.4    def pad_x: Double = char_width * 1.5
     4.5    def pad_y: Double = char_width
     4.6  
     4.7 +  def dummy_width2: Double = (pad_x / 2).ceil
     4.8 +
     4.9    def box_width2(node: Graph_Display.Node): Double =
    4.10      ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
    4.11 +
    4.12 +  def box_width2(vertex: Layout.Vertex): Double =
    4.13 +    vertex match {
    4.14 +      case Layout.Node(node) => box_width2(node)
    4.15 +      case _: Layout.Dummy => dummy_width2
    4.16 +    }
    4.17    def box_gap: Double = gap.ceil
    4.18    def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
    4.19  }
     5.1 --- a/src/Tools/Graphview/shapes.scala	Tue Jan 06 11:58:57 2015 +0100
     5.2 +++ b/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:33:30 2015 +0100
     5.3 @@ -24,11 +24,11 @@
     5.4      def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
     5.5      {
     5.6        val metrics = visualizer.metrics
     5.7 -      val p = visualizer.Coordinates.get_node(node)
     5.8 +      val p = visualizer.get_vertex(Layout.Node(node))
     5.9        val bounds = metrics.string_bounds(node.toString)
    5.10 -      val w = bounds.getWidth + metrics.pad_x
    5.11 -      val h = bounds.getHeight + metrics.pad_y
    5.12 -      new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
    5.13 +      val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil
    5.14 +      val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil
    5.15 +      new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2)
    5.16      }
    5.17  
    5.18      def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
    5.19 @@ -58,8 +58,8 @@
    5.20      def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
    5.21      {
    5.22        val metrics = visualizer.metrics
    5.23 -      val w = metrics.pad_x
    5.24 -      new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
    5.25 +      val w = metrics.dummy_width2
    5.26 +      new Rectangle2D.Double(d.x - w / 2, d.y - w / 2, w, w)
    5.27      }
    5.28  
    5.29      def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
    5.30 @@ -74,13 +74,13 @@
    5.31    {
    5.32      def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
    5.33      {
    5.34 -      val p = visualizer.Coordinates.get_node(edge._1)
    5.35 -      val q = visualizer.Coordinates.get_node(edge._2)
    5.36 +      val p = visualizer.get_vertex(Layout.Node(edge._1))
    5.37 +      val q = visualizer.get_vertex(Layout.Node(edge._2))
    5.38        val ds =
    5.39        {
    5.40          val a = p.y min q.y
    5.41          val b = p.y max q.y
    5.42 -        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
    5.43 +        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    5.44        }
    5.45        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
    5.46  
    5.47 @@ -106,13 +106,13 @@
    5.48  
    5.49      def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
    5.50      {
    5.51 -      val p = visualizer.Coordinates.get_node(edge._1)
    5.52 -      val q = visualizer.Coordinates.get_node(edge._2)
    5.53 +      val p = visualizer.get_vertex(Layout.Node(edge._1))
    5.54 +      val q = visualizer.get_vertex(Layout.Node(edge._2))
    5.55        val ds =
    5.56        {
    5.57          val a = p.y min q.y
    5.58          val b = p.y max q.y
    5.59 -        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
    5.60 +        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    5.61        }
    5.62  
    5.63        if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
     6.1 --- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 11:58:57 2015 +0100
     6.2 +++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:33:30 2015 +0100
     6.3 @@ -19,11 +19,57 @@
     6.4  {
     6.5    visualizer =>
     6.6  
     6.7 +
     6.8 +  /* layout state */
     6.9 +
    6.10    // owned by GUI thread
    6.11    private var layout: Layout = Layout.empty
    6.12  
    6.13    def metrics: Metrics = layout.metrics
    6.14 -  def visible_graph: Graph_Display.Graph = layout.visible_graph
    6.15 +  def visible_graph: Graph_Display.Graph = layout.input_graph
    6.16 +
    6.17 +  def get_vertex(v: Layout.Vertex): Layout.Point = layout.get_vertex(v)
    6.18 +  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double)
    6.19 +  {
    6.20 +    layout = layout.translate_vertex(v, dx, dy)
    6.21 +  }
    6.22 +
    6.23 +  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
    6.24 +    layout.dummies_iterator(edge)
    6.25 +
    6.26 +  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
    6.27 +    layout.find_dummy(pred)
    6.28 +
    6.29 +  def bounding_box(): Rectangle2D.Double =
    6.30 +  {
    6.31 +    var x0 = 0.0
    6.32 +    var y0 = 0.0
    6.33 +    var x1 = 0.0
    6.34 +    var y1 = 0.0
    6.35 +    ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
    6.36 +     (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
    6.37 +       foreach(rect => {
    6.38 +          x0 = x0 min rect.getMinX
    6.39 +          y0 = y0 min rect.getMinY
    6.40 +          x1 = x1 max rect.getMaxX
    6.41 +          y1 = y1 max rect.getMaxY
    6.42 +        })
    6.43 +    val gap = metrics.gap
    6.44 +    x0 = (x0 - gap).floor
    6.45 +    y0 = (y0 - gap).floor
    6.46 +    x1 = (x1 + gap).ceil
    6.47 +    y1 = (y1 + gap).ceil
    6.48 +    new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
    6.49 +  }
    6.50 +
    6.51 +  def update_layout()
    6.52 +  {
    6.53 +    val metrics = Metrics(make_font())
    6.54 +    val visible_graph = model.make_visible_graph()
    6.55 +
    6.56 +    // FIXME avoid expensive operation on GUI thread
    6.57 +    layout = Layout.make(metrics, visible_graph)
    6.58 +  }
    6.59  
    6.60  
    6.61    /* tooltips */
    6.62 @@ -85,60 +131,6 @@
    6.63        Shapes.Node.paint(gfx, visualizer, node)
    6.64    }
    6.65  
    6.66 -  object Coordinates
    6.67 -  {
    6.68 -    def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node)
    6.69 -    def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge)
    6.70 -
    6.71 -    def translate_node(node: Graph_Display.Node, dx: Double, dy: Double)
    6.72 -    {
    6.73 -      layout = layout.map_node(node, p => Layout.Point(p.x + dx, p.y + dy))
    6.74 -    }
    6.75 -
    6.76 -    def translate_dummy(d: (Graph_Display.Edge, Int), dx: Double, dy: Double)
    6.77 -    {
    6.78 -      val (edge, index) = d
    6.79 -      layout = layout.map_dummies(edge,
    6.80 -        ds => {
    6.81 -          val p = ds(index)
    6.82 -          (ds.zipWithIndex :\ List.empty[Layout.Point]) {
    6.83 -            case ((t, i), n) => if (index == i) Layout.Point(p.x + dx, p.y + dy) :: n else t :: n
    6.84 -          }
    6.85 -        })
    6.86 -    }
    6.87 -
    6.88 -    def update_layout()
    6.89 -    {
    6.90 -      val metrics = Metrics(make_font())
    6.91 -      val visible_graph = model.make_visible_graph()
    6.92 -
    6.93 -      // FIXME avoid expensive operation on GUI thread
    6.94 -      layout = Layout.make(metrics, visible_graph)
    6.95 -    }
    6.96 -
    6.97 -    def bounding_box(): Rectangle2D.Double =
    6.98 -    {
    6.99 -      var x0 = 0.0
   6.100 -      var y0 = 0.0
   6.101 -      var x1 = 0.0
   6.102 -      var y1 = 0.0
   6.103 -      ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
   6.104 -       (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
   6.105 -         foreach(rect => {
   6.106 -            x0 = x0 min rect.getMinX
   6.107 -            y0 = y0 min rect.getMinY
   6.108 -            x1 = x1 max rect.getMaxX
   6.109 -            y1 = y1 max rect.getMaxY
   6.110 -          })
   6.111 -      val gap = metrics.gap
   6.112 -      x0 = (x0 - gap).floor
   6.113 -      y0 = (y0 - gap).floor
   6.114 -      x1 = (x1 + gap).ceil
   6.115 -      y1 = (y1 + gap).ceil
   6.116 -      new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
   6.117 -    }
   6.118 -  }
   6.119 -
   6.120    object Selection
   6.121    {
   6.122      // owned by GUI thread