# HG changeset patch
# User wenzelm
# Date 1420412821 -3600
# Node ID 962ad3942ea7656c0f124f42cd336dad85a3abe8
# Parent  fecf1d5a2454c6c6da98543dcb83df86d524c7cf
more metrics, with integer coordinates for layout;
initial coordinates: center x as in old browser;
Layout.pendulum/collapse: proper downwards range;
distance as in old browser (see spaceBetween);
move offset as in old browser;
more careful comparison wrt. 0.0 (this is IEEE double, not int);

diff -r fecf1d5a2454 -r 962ad3942ea7 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sun Jan 04 21:53:05 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Jan 05 00:07:01 2015 +0100
@@ -36,15 +36,6 @@
   {
     if (visible_graph.is_empty) empty
     else {
-      def box_width(key: Key): Double =
-        (metrics.string_bounds(key.toString).getWidth + metrics.pad).ceil
-
-      val box_distance = (visible_graph.keys_iterator.map(box_width(_)).max + metrics.gap).ceil
-
-      def box_height(level: Level): Double =
-        (metrics.char_width * 1.5 * (5 max level.length)).ceil
-
-
       val initial_levels = level_map(visible_graph)
 
       val (dummy_graph, dummies, dummy_levels) =
@@ -64,11 +55,14 @@
         (((Map.empty[Key, Point], 0.0) /: levels) {
           case ((coords1, y), level) =>
             ((((coords1, 0.0) /: level) {
-              case ((coords2, x), key) => (coords2 + (key -> Point(x, y)), x + box_distance)
-            })._1, y + box_height(level))
+              case ((coords2, x), key) =>
+                val w2 = metrics.box_width2(key)
+                (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
+            })._1, y + metrics.box_height(level.length))
         })._1
 
-      val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)
+
+      val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates)
 
       val dummy_coords =
         (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
@@ -87,7 +81,7 @@
       ((levels(from) + 1) until levels(to)).map(l => {
           // FIXME !?
           val ident = "%s$%s$%d".format(from.ident, to.ident, l)
-          Graph_Display.Node(ident, ident)
+          Graph_Display.Node(" ", ident)
         }).toList
 
     val ls =
@@ -175,7 +169,8 @@
     }._1
   }
 
-  def pendulum(graph: Graph_Display.Graph, box_distance: Double,
+  def pendulum(
+    metrics: Visualizer.Metrics, graph: Graph_Display.Graph,
     levels: Levels, coords: Map[Key, Point]): Coordinates =
   {
     type Regions = List[List[Region]]
@@ -201,15 +196,15 @@
         var regions_changed = true
         while (regions_changed) {
           regions_changed = false
-          for (i <- (next.length to 1)) {
-            val (r1, r2) = (next(i-1), next(i))
-            val d1 = r1.deflection(coords, top_down)
-            val d2 = r2.deflection(coords, top_down)
+          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)
 
             if (// Do regions touch?
-                r1.distance(coords, r2) <= box_distance &&
+                r1.distance(metrics, coords, r2) <= 0.0 &&
                 // Do they influence each other?
-                (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0))
+                (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
@@ -227,25 +222,18 @@
       ((coords, false) /: (0 until level.length)) {
         case ((coords, moved), i) =>
           val r = level(i)
-          val d = r.deflection(coords, top_down)
+          val d = r.deflection(graph, coords, top_down)
           val offset =
-          {
-            if (i == 0 && d <= 0) d
-            else if (i == level.length - 1 && d >= 0) d
-            else if (d < 0) {
-              val prev = level(i - 1)
-              (- (r.distance(coords, prev) - box_distance)) max d
-            }
-            else {
-              val next = level(i + 1)
-              (r.distance(coords, next) - box_distance) min d
-            }
-          }
+            if (d < 0 && i > 0)
+              - (level(i - 1).distance(metrics, coords, r) min (- d))
+            else if (d >= 0 && i < level.length - 1)
+              r.distance(metrics, coords, level(i + 1)) min d
+            else d
           (r.move(coords, offset), moved || d != 0)
       }
     }
 
-    val regions = levels.map(level => level.map(new Region(graph, _)))
+    val regions = levels.map(level => level.map(new Region(_)))
 
     ((coords, regions, true, true) /: (1 to pendulum_iterations)) {
       case ((coords, regions, top_down, moved), _) =>
@@ -260,30 +248,32 @@
   /*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(val graph: Graph_Display.Graph, node: Key)
+  private class Region(node: Key)
   {
     var nodes: List[Key] = List(node)
 
-    def left(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).min
-    def right(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).max
+    def distance(metrics: Visualizer.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 distance(coords: Coordinates, to: Region): Double =
-      math.abs(left(coords) - to.left(coords)) min
-      math.abs(right(coords) - to.right(coords))
-
-    def deflection(coords: Coordinates, top_down: Boolean): Double =
-      (for (a <- nodes.iterator) yield {
+    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
+      }).sum / nodes.length).round.toDouble
 
     def move(coords: Coordinates, dx: Double): Coordinates =
-      (coords /: nodes) {
-        case (cs, node) =>
-          val p = cs(node)
-          cs + (node -> Point(p.x + dx, p.y))
-      }
+      if (dx == 0.0) coords
+      else
+        (coords /: nodes) {
+          case (cs, node) =>
+            val p = cs(node)
+            cs + (node -> Point(p.x + dx, p.y))
+        }
   }
 }
 
diff -r fecf1d5a2454 -r 962ad3942ea7 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 04 21:53:05 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 00:07:01 2015 +0100
@@ -38,6 +38,11 @@
     def ascent: Double = font.getLineMetrics("", font_render_context).getAscent
     def gap: Double = mix.getWidth
     def pad: Double = char_width
+
+    def box_width2(node: Graph_Display.Node): Double =
+      ((string_bounds(node.toString).getWidth + pad) / 2).ceil
+    def box_gap: Double = gap.ceil
+    def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
   }
 }