author wenzelm Tue, 06 Jan 2015 22:34:26 +0100 changeset 59307 b5d1b8175b8e parent 59306 cd2a0c14fe66 child 59308 9479766b9418
rubberband method as in old browser; tuned;
```--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 20:12:46 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 22:34:26 2015 +0100
@@ -2,7 +2,7 @@
Author:     Markus Kaiser, TU Muenchen
Author:     Makarius

-DAG layout algorithm, according to:
+DAG layout according to:

Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
@@ -58,12 +58,25 @@
val empty_graph: Graph = make_graph(Nil)

+  /* vertex x coordinate */
+
+  private def vertex_left(metrics: Metrics, graph: Graph, v: Vertex): Double =
+    graph.get_node(v).x - metrics.box_width2(v)
+
+  private def vertex_right(metrics: Metrics, graph: Graph, v: Vertex): Double =
+    graph.get_node(v).x + metrics.box_width2(v)
+
+  private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
+    if (dx == 0.0) graph else graph.map_node(v, p => Point(p.x + dx, p.y))
+
+
/* layout */

val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)

+  val minimize_crossings_iterations = 40
val pendulum_iterations = 10
-  val minimize_crossings_iterations = 40
+  val rubberband_iterations = 10

private type Levels = Map[Vertex, Int]
@@ -128,9 +141,11 @@
})._1

-      /* pendulum layout */
+      /* pendulum/rubberband layout */

-      val output_graph = pendulum(metrics, levels_graph, levels)
+      val output_graph =
+        rubberband(metrics, levels,
+          pendulum(metrics, levels, levels_graph))

new Layout(metrics, input_graph, output_graph)
}
@@ -142,7 +157,7 @@

private type Level = List[Vertex]

-  def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
+  private def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
{
def resort(parent: Level, child: Level, top_down: Boolean): Level =
child.map(v => {
@@ -171,7 +186,7 @@
}._1
}

-  def level_list(levels: Levels): List[Level] =
+  private def level_list(levels: Levels): List[Level] =
{
val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
val buckets = new Array[Level](max_lev + 1)
@@ -180,7 +195,7 @@
buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
}

-  def count_crossings(graph: Graph, levels: List[Level]): Int =
+  private def count_crossings(graph: Graph, levels: List[Level]): Int =
{
def in_level(ls: List[Level]): Int = ls match {
case List(top, bot) =>
@@ -215,11 +230,9 @@
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
-    }
+      vertex_right(metrics, graph, this.content.last) -
+      metrics.box_gap

def deflection(graph: Graph, top_down: Boolean): Double =
((for (a <- content.iterator) yield {
@@ -229,13 +242,12 @@
}).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)) }
+      if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
}

private type Regions = List[List[Region]]

-  def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
+  private def pendulum(metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
{
def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
{
@@ -304,6 +316,43 @@
else (graph, regions, !top_down, moved)
}._1
}
+
+
+
+  /** rubberband method **/
+
+  private def force_weight(graph: Graph, v: Vertex): Double =
+  {
+    val preds = graph.imm_preds(v)
+    val succs = graph.imm_succs(v)
+    val n = preds.size + succs.size
+    if (n == 0) 0.0
+    else {
+      val x = graph.get_node(v).x
+      ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
+    }
+  }
+
+  private def rubberband(metrics: Metrics, levels: List[Level], graph: Graph): Graph =
+  {
+    val gap = metrics.box_gap
+    def left(g: Graph, v: Vertex) = vertex_left(metrics, g, v)
+    def right(g: Graph, v: Vertex) = vertex_right(metrics, g, v)
+
+    (graph /: (1 to rubberband_iterations)) { case (graph, _) =>
+      (graph /: levels) { case (graph, level) =>
+        val m = level.length - 1
+        (graph /: level.iterator.zipWithIndex) {
+          case (g, (v, i)) =>
+            val d = force_weight(g, v)
+            if (d < 0.0 && (i == 0 || right(g, level(i - 1)) + gap < left(g, v) + d) ||
+                d > 0.0 && (i == m || left(g, level(i + 1)) - gap > right(g, v) + d))
+              move_vertex(g, v, d.round.toDouble)
+            else g
+        }
+      }
+    }
+  }
}

final class Layout private(```