--- a/src/Tools/Graphview/layout.scala Mon Mar 01 22:22:12 2021 +0100
+++ b/src/Tools/Graphview/layout.scala Mon Mar 01 22:26:33 2021 +0100
@@ -294,10 +294,12 @@
val r = level(i)
val d = r.deflection(graph, top_down)
val dx =
- if (d < 0.0 && i > 0)
+ if (d < 0.0 && i > 0) {
- (level(i - 1).distance(metrics, graph, r) min (- d))
- else if (d >= 0.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, dx), moved || d != 0.0)
}