--- a/src/Tools/Graphview/src/layout_pendulum.scala Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala Mon Oct 08 23:29:07 2012 +0200
@@ -22,12 +22,15 @@
val x_distance = 350
val y_distance = 350
val pendulum_iterations = 10
+ val minimize_crossings_iterations = 40
- def apply(graph: Model.Graph): Layout = {
- if (graph.entries.isEmpty)
+ def apply(graph: Model.Graph): Layout =
+ {
+ if (graph.is_empty)
(Map[Key, Point](), Map[(Key, Key), List[Point]]())
else {
- val (dummy_graph, dummies, dummy_levels) = {
+ val (dummy_graph, dummies, dummy_levels) =
+ {
val initial_levels = level_map(graph)
def add_dummies(graph: Model.Graph, from: Key, to: Key,
@@ -79,7 +82,7 @@
initial_coordinates(levels)
)
- val dummy_coords =
+ val dummy_coords =
(Map[(Key, Key), List[Point]]() /: dummies.keys) {
case (map, key) => map + (key -> dummies(key).map(coords(_)))
}
@@ -87,32 +90,30 @@
(coords, dummy_coords)
}
}
-
+
def level_map(graph: Model.Graph): Map[Key, Int] =
- (Map[Key, Int]() /: graph.topological_order){
+ (Map[Key, Int]() /: graph.topological_order) {
(levels, key) => {
- val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
- levels + (key -> (pred_levels.max + 1))
- }}
+ val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
+ levels + (key -> lev)
+ }
+ }
def level_list(map: Map[Key, Int]): Levels =
- (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
- case ((key, i), list) => {
- if (list.isEmpty) (i, List(key)) :: list
- else {
- val (j, l) = list.head
- if (i == j) (i, key :: l) :: list.tail
- else (i, List(key)) :: list
- }
- }
- }.map(_._2)
-
+ {
+ val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
+ val buckets = new Array[Level](max_lev + 1)
+ for (l <- 0 to max_lev) { buckets(l) = Nil }
+ for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
+ buckets.iterator.map(_.sorted).toList
+ }
+
def count_crossings(graph: Model.Graph, levels: Levels): Int = {
def in_level(ls: Levels): Int = ls match {
case List(top, bot) =>
top.zipWithIndex.map{
case (outer_parent, outer_parent_index) =>
- graph.imm_succs(outer_parent).map(bot.indexOf(_))
+ graph.imm_succs(outer_parent).map(bot.indexOf(_)) // FIXME iterator
.map(outer_child => {
(0 until outer_parent_index)
.map(inner_parent =>
@@ -153,11 +154,11 @@
}
}
- ((levels, count_crossings(graph, levels), true) /: (1 to 40)) {
+ ((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)
+ if (new_crossings < old_crossings)
(new_levels, new_crossings, !top_down)
else
(old_levels, old_crossings, !top_down)
@@ -250,7 +251,7 @@
val regions = levels.map(level => level.map(new Region(graph, _)))
((regions, coords, true, true) /: (1 to pendulum_iterations)) {
- case ((regions, coords, top_down, moved), _) =>
+ case ((regions, coords, top_down, moved), i) =>
if (moved) {
val (nextr, nextc, m) = iteration(regions, coords, top_down)
(nextr, nextc, !top_down, m)
@@ -272,7 +273,7 @@
def deflection(coords: Coordinates, use_preds: Boolean) =
nodes.map(k => (coords(k)._1,
- if (use_preds) graph.imm_preds(k).toList
+ if (use_preds) graph.imm_preds(k).toList // FIXME iterator
else graph.imm_succs(k).toList))
.map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
.sum / nodes.length