# HG changeset patch
# User wenzelm
# Date 1420583006 -3600
# Node ID 7cdabe4cec33b8adae2962de4e914c09ab4766e0
# Parent  e8189de55b65413b7b40e6652752069f1870839b
tuned;

diff -r e8189de55b65 -r 7cdabe4cec33 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 22:51:00 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 23:23:26 2015 +0100
@@ -196,27 +196,16 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-  {
-    def in_level(ls: List[Level]): Int = ls match {
+    levels.iterator.sliding(2).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
-            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
-            .map(outer_child =>
-              (0 until outer_parent_index)
-              .map(inner_parent =>
-                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
-                .filter(inner_child => outer_child < inner_child)
-                .size
-              ).sum
-            ).sum
+            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
+              (0 until outer_parent_index).iterator.map(inner_parent =>
+                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)).
+                  filter(inner_child => outer_child < inner_child).size).sum).sum
         }.sum
-
-      case _ => 0
-    }
-
-    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
-  }
+    }.sum