# HG changeset patch
# User wenzelm
# Date 1420584973 -3600
# Node ID c4b9b04bfc6d1ff6c458cb1ad132fbde314c1404
# Parent  a269cc01e8eb1401133cfc3a30217abd107499cf
proper level distance according to number of edges, as in old browser;

diff -r a269cc01e8eb -r c4b9b04bfc6d src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 23:35:57 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 23:56:13 2015 +0100
@@ -141,11 +141,12 @@
       val levels_graph: Graph =
         (((dummy_graph, 0.0) /: levels) {
           case ((graph, y), level) =>
+            val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
             ((((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, y + metrics.box_height(num_edges))
         })._1