tuned --- silence odd warning;

--- 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)
       }