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

--- a/src/Tools/Graphview/layout.scala	Fri Apr 08 16:42:52 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 11:41:37 2022 +0200
@@ -235,7 +235,7 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-    levels.iterator.sliding(2).map {
+    levels.iterator.sliding(2).map(_.toList).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>