# HG changeset patch
# User wenzelm
# Date 1420571566 -3600
# Node ID cd2a0c14fe66bfe636a04c644bd4e1b7459e9f49
# Parent  b5e33012180ee9ef1e815987a52abd8a006ad77c
tuned;

diff -r b5e33012180e -r cd2a0c14fe66 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 17:08:18 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 20:12:46 2015 +0100
@@ -144,7 +144,7 @@
 
   def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
   {
-    def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
+    def resort(parent: Level, child: Level, top_down: Boolean): Level =
       child.map(v => {
           val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
           val weight =
@@ -152,25 +152,22 @@
           (v, weight)
       }).sortBy(_._2).map(_._1)
 
-    def resort(levels: List[Level], top_down: Boolean) =
-      if (top_down)
-        (List(levels.head) /: levels.tail)((tops, bot) =>
-          resort_level(tops.head, bot, top_down) :: tops).reverse
-      else {
-        val rev_levels = levels.reverse
-        (List(rev_levels.head) /: rev_levels.tail)((bots, top) =>
-          resort_level(bots.head, top, top_down) :: bots)
-      }
-
     ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
-      case ((old_levels, old_crossings, top_down), _) => {
-          val new_levels = resort(old_levels, top_down)
-          val new_crossings = count_crossings(graph, new_levels)
-          if (new_crossings < old_crossings)
-            (new_levels, new_crossings, !top_down)
-          else
-            (old_levels, old_crossings, !top_down)
-      }
+      case ((old_levels, old_crossings, top_down), _) =>
+        val new_levels =
+          if (top_down)
+            (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
+              resort(tops.head, bot, top_down) :: tops).reverse
+          else {
+            val rev_old_levels = old_levels.reverse
+            (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
+              resort(bots.head, top, top_down) :: bots)
+          }
+        val new_crossings = count_crossings(graph, new_levels)
+        if (new_crossings < old_crossings)
+          (new_levels, new_crossings, !top_down)
+        else
+          (old_levels, old_crossings, !top_down)
     }._1
   }