src/Tools/Graphview/layout.scala

--- a/src/Tools/Graphview/layout.scala	Sat Apr 09 11:45:39 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 11:56:48 2022 +0200
@@ -137,7 +137,7 @@
 
               val levels1 = dummies_levels.foldLeft(levels)(_ + _)
               val graph1 =
-                (v1 :: dummies ::: List(v2)).sliding(2).
+                (v1 :: dummies ::: List(v2)).sliding(2).map(_.toList).
                   foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
                     case (g, List(a, b)) => g.add_edge(a, b)
                   }