# HG changeset patch
# User wenzelm
# Date 1649498208 -7200
# Node ID 5f8f0bf8c72c2b366a360ef8192912180f26dcf2
# Parent  d164bf04d05e0dfca34247886a9d6987c35fec46
proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

diff -r d164bf04d05e -r 5f8f0bf8c72c 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)
                   }
diff -r d164bf04d05e -r 5f8f0bf8c72c src/Tools/Graphview/shapes.scala
--- 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