--- a/src/Tools/Graphview/layout.scala Sun Jan 04 21:53:05 2015 +0100
+++ b/src/Tools/Graphview/layout.scala Mon Jan 05 00:07:01 2015 +0100
@@ -36,15 +36,6 @@
{
if (visible_graph.is_empty) empty
else {
- def box_width(key: Key): Double =
- (metrics.string_bounds(key.toString).getWidth + metrics.pad).ceil
-
- val box_distance = (visible_graph.keys_iterator.map(box_width(_)).max + metrics.gap).ceil
-
- def box_height(level: Level): Double =
- (metrics.char_width * 1.5 * (5 max level.length)).ceil
-
-
val initial_levels = level_map(visible_graph)
val (dummy_graph, dummies, dummy_levels) =
@@ -64,11 +55,14 @@
(((Map.empty[Key, Point], 0.0) /: levels) {
case ((coords1, y), level) =>
((((coords1, 0.0) /: level) {
- case ((coords2, x), key) => (coords2 + (key -> Point(x, y)), x + box_distance)
- })._1, y + box_height(level))
+ case ((coords2, x), key) =>
+ val w2 = metrics.box_width2(key)
+ (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
+ })._1, y + metrics.box_height(level.length))
})._1
- val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)
+
+ val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates)
val dummy_coords =
(Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
@@ -87,7 +81,7 @@
((levels(from) + 1) until levels(to)).map(l => {
// FIXME !?
val ident = "%s$%s$%d".format(from.ident, to.ident, l)
- Graph_Display.Node(ident, ident)
+ Graph_Display.Node(" ", ident)
}).toList
val ls =
@@ -175,7 +169,8 @@
}._1
}
- def pendulum(graph: Graph_Display.Graph, box_distance: Double,
+ def pendulum(
+ metrics: Visualizer.Metrics, graph: Graph_Display.Graph,
levels: Levels, coords: Map[Key, Point]): Coordinates =
{
type Regions = List[List[Region]]
@@ -201,15 +196,15 @@
var regions_changed = true
while (regions_changed) {
regions_changed = false
- for (i <- (next.length to 1)) {
- val (r1, r2) = (next(i-1), next(i))
- val d1 = r1.deflection(coords, top_down)
- val d2 = r2.deflection(coords, top_down)
+ for (i <- Range(next.length - 1, 0, -1)) {
+ val (r1, r2) = (next(i - 1), next(i))
+ val d1 = r1.deflection(graph, coords, top_down)
+ val d2 = r2.deflection(graph, coords, top_down)
if (// Do regions touch?
- r1.distance(coords, r2) <= box_distance &&
+ r1.distance(metrics, coords, r2) <= 0.0 &&
// Do they influence each other?
- (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0))
+ (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
{
regions_changed = true
r1.nodes = r1.nodes ::: r2.nodes
@@ -227,25 +222,18 @@
((coords, false) /: (0 until level.length)) {
case ((coords, moved), i) =>
val r = level(i)
- val d = r.deflection(coords, top_down)
+ val d = r.deflection(graph, coords, top_down)
val offset =
- {
- if (i == 0 && d <= 0) d
- else if (i == level.length - 1 && d >= 0) d
- else if (d < 0) {
- val prev = level(i - 1)
- (- (r.distance(coords, prev) - box_distance)) max d
- }
- else {
- val next = level(i + 1)
- (r.distance(coords, next) - box_distance) min d
- }
- }
+ if (d < 0 && i > 0)
+ - (level(i - 1).distance(metrics, coords, r) min (- d))
+ else if (d >= 0 && i < level.length - 1)
+ r.distance(metrics, coords, level(i + 1)) min d
+ else d
(r.move(coords, offset), moved || d != 0)
}
}
- val regions = levels.map(level => level.map(new Region(graph, _)))
+ val regions = levels.map(level => level.map(new Region(_)))
((coords, regions, true, true) /: (1 to pendulum_iterations)) {
case ((coords, regions, top_down, moved), _) =>
@@ -260,30 +248,32 @@
/*This is an auxiliary class which is used by the layout algorithm when
calculating coordinates with the "pendulum method". A "region" is a
group of nodes which "stick together".*/
- private class Region(val graph: Graph_Display.Graph, node: Key)
+ private class Region(node: Key)
{
var nodes: List[Key] = List(node)
- def left(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).min
- def right(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).max
+ def distance(metrics: Visualizer.Metrics, coords: Coordinates, that: Region): Double =
+ {
+ val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1)
+ val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2)
+ x2 - x1 - metrics.box_gap
+ }
- def distance(coords: Coordinates, to: Region): Double =
- math.abs(left(coords) - to.left(coords)) min
- math.abs(right(coords) - to.right(coords))
-
- def deflection(coords: Coordinates, top_down: Boolean): Double =
- (for (a <- nodes.iterator) yield {
+ def deflection(graph: Graph_Display.Graph, coords: Coordinates, top_down: Boolean): Double =
+ ((for (a <- nodes.iterator) yield {
val x = coords(a).x
val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
bs.iterator.map(coords(_).x - x).sum / (bs.size max 1)
- }).sum / nodes.length
+ }).sum / nodes.length).round.toDouble
def move(coords: Coordinates, dx: Double): Coordinates =
- (coords /: nodes) {
- case (cs, node) =>
- val p = cs(node)
- cs + (node -> Point(p.x + dx, p.y))
- }
+ if (dx == 0.0) coords
+ else
+ (coords /: nodes) {
+ case (cs, node) =>
+ val p = cs(node)
+ cs + (node -> Point(p.x + dx, p.y))
+ }
}
}