# HG changeset patch # User wenzelm # Date 1420636746 -3600 # Node ID a1238edd8b3684cbab403870eb121bbe386a4c79 # Parent 2f4d64fba0d75bb66875b3c0e251b127fcd6f237 tuned; diff -r 2f4d64fba0d7 -r a1238edd8b36 src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala Wed Jan 07 14:06:52 2015 +0100 +++ b/src/Tools/Graphview/layout.scala Wed Jan 07 14:19:06 2015 +0100 @@ -269,13 +269,13 @@ case ((graph, moved), i) => val r = level(i) val d = r.deflection(graph, top_down) - val offset = - if (d < 0 && i > 0) + val dx = + if (d < 0.0 && i > 0) - (level(i - 1).distance(metrics, graph, r) min (- d)) - else if (d >= 0 && i < level.length - 1) + else if (d >= 0.0 && i < level.length - 1) r.distance(metrics, graph, level(i + 1)) min d else d - (r.move(graph, offset), moved || d != 0) + (r.move(graph, dx), moved || d != 0.0) } }