# HG changeset patch
# User wenzelm
# Date 1649507374 -7200
# Node ID f6ee58333aa5332efda3dd92d5cc36dac244d42c
# Parent  320f413fe4b9917a9204c0832bad665af3ae4a35
clarified signature;

diff -r 320f413fe4b9 -r f6ee58333aa5 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sat Apr 09 12:35:48 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 14:29:34 2022 +0200
@@ -137,9 +137,9 @@
 
               val levels1 = dummies_levels.foldLeft(levels)(_ + _)
               val graph1 =
-                (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)
+                (v1 :: dummies ::: List(v2)).sliding(2)
+                  .foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
+                    case (g, Seq(a, b)) => g.add_edge(a, b)
                     case _ => ???
                   }
               (graph1, levels1)
@@ -236,8 +236,8 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-    levels.iterator.sliding(2).map(_.toList).map {
-      case List(top, bot) =>
+    levels.iterator.sliding(2).map {
+      case Seq(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
             graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
diff -r 320f413fe4b9 -r f6ee58333aa5 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Apr 09 12:35:48 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 09 14:29:34 2022 +0200
@@ -116,8 +116,8 @@
         val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          coords.sliding(3).map(_.toList).foldLeft((dx, dy)) {
-            case ((dx, dy), List(l, m, r)) =>
+          coords.sliding(3).foldLeft((dx, dy)) {
+            case ((dx, dy), Seq(l, m, r)) =>
               val dx2 = r.x - l.x
               val dy2 = r.y - l.y
               path.curveTo(