proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

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

--- a/src/Tools/Graphview/shapes.scala	Sat Apr 09 11:45:39 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 09 11:56:48 2022 +0200
@@ -116,7 +116,7 @@
         val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          coords.sliding(3).foldLeft((dx, dy)) {
+          coords.sliding(3).map(_.toList).foldLeft((dx, dy)) {
             case ((dx, dy), List(l, m, r)) =>
               val dx2 = r.x - l.x
               val dy2 = r.y - l.y