--- 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 =>