# HG changeset patch
# User wenzelm
# Date 1420580066 -3600
# Node ID b5d1b8175b8e936bdd4ff721da9b8b5a97d66119
# Parent  cd2a0c14fe66bfe636a04c644bd4e1b7459e9f49
rubberband method as in old browser;
tuned;

diff -r cd2a0c14fe66 -r b5d1b8175b8e src/Tools/Graphview/layout.scala
--- 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_left(metrics, graph, that.content.head) -
+      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(