author | wenzelm |
Tue, 06 Jan 2015 23:56:13 +0100 | |
changeset 59312 | c4b9b04bfc6d |
parent 59311 | a269cc01e8eb |
child 59313 | d7f4f46e9a59 |
permissions | -rw-r--r-- |
59232 | 1 |
/* Title: Tools/Graphview/layout.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
59240 | 3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
59307 | 5 |
DAG layout according to: |
59261 | 6 |
|
7 |
Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing, |
|
8 |
DIMACS International Workshop (GD'94), Springer LNCS 894, 1995. |
|
9 |
||
10 |
http://dx.doi.org/10.1007/3-540-58950-3_371 |
|
11 |
ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
import isabelle._ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
19 |
|
59232 | 20 |
object Layout |
49744 | 21 |
{ |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
22 |
/* graph structure */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
23 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
24 |
object Vertex |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
25 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
26 |
object Ordering extends scala.math.Ordering[Vertex] |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
27 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
28 |
def compare(v1: Vertex, v2: Vertex): Int = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
29 |
(v1, v2) match { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
30 |
case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
31 |
case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
32 |
Graph_Display.Node.Ordering.compare(a1, b1) match { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
33 |
case 0 => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
34 |
Graph_Display.Node.Ordering.compare(a2, b2) match { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
35 |
case 0 => i compare j |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
36 |
case ord => ord |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
37 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
38 |
case ord => ord |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
39 |
} |
59311
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
40 |
case (Node(a), Dummy(b, _, _)) => |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
41 |
Graph_Display.Node.Ordering.compare(a, b) match { |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
42 |
case 0 => -1 |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
43 |
case ord => ord |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
44 |
} |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
45 |
case (Dummy(a, _, _), Node(b)) => |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
46 |
Graph_Display.Node.Ordering.compare(a, b) match { |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
47 |
case 0 => 1 |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
48 |
case ord => ord |
a269cc01e8eb
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents:
59310
diff
changeset
|
49 |
} |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
50 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
51 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
52 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
53 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
54 |
sealed abstract class Vertex |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
55 |
case class Node(node: Graph_Display.Node) extends Vertex |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
56 |
case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
57 |
|
59262 | 58 |
object Point { val zero: Point = Point(0.0, 0.0) } |
59 |
case class Point(x: Double, y: Double) |
|
50469 | 60 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
61 |
type Graph = isabelle.Graph[Vertex, Point] |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
62 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
63 |
def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
64 |
isabelle.Graph.make(entries)(Vertex.Ordering) |
59262 | 65 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
66 |
val empty_graph: Graph = make_graph(Nil) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
67 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
68 |
|
59307 | 69 |
/* vertex x coordinate */ |
70 |
||
71 |
private def vertex_left(metrics: Metrics, graph: Graph, v: Vertex): Double = |
|
72 |
graph.get_node(v).x - metrics.box_width2(v) |
|
73 |
||
74 |
private def vertex_right(metrics: Metrics, graph: Graph, v: Vertex): Double = |
|
75 |
graph.get_node(v).x + metrics.box_width2(v) |
|
76 |
||
77 |
private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph = |
|
78 |
if (dx == 0.0) graph else graph.map_node(v, p => Point(p.x + dx, p.y)) |
|
79 |
||
80 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
81 |
/* layout */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
82 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
83 |
val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) |
50470 | 84 |
|
59307 | 85 |
val minimize_crossings_iterations = 40 |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
86 |
val pendulum_iterations = 10 |
59307 | 87 |
val rubberband_iterations = 10 |
50469 | 88 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
89 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
90 |
private type Levels = Map[Vertex, Int] |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
91 |
private val empty_levels: Levels = Map.empty |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
92 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
93 |
def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout = |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
94 |
{ |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
95 |
if (input_graph.is_empty) empty |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
96 |
else { |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
97 |
/* initial graph */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
98 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
99 |
val initial_graph = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
100 |
make_graph( |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
101 |
input_graph.iterator.map( |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
102 |
{ case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
103 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
104 |
val initial_levels: Levels = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
105 |
(empty_levels /: initial_graph.topological_order) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
106 |
case (levels, vertex) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
107 |
val level = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
108 |
1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
109 |
levels + (vertex -> level) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
110 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
111 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
112 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
113 |
/* graph with dummies */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
114 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
115 |
val (dummy_graph, dummy_levels) = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
116 |
((initial_graph, initial_levels) /: input_graph.edges_iterator) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
117 |
case ((graph, levels), (node1, node2)) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
118 |
val v1 = Node(node1); val l1 = levels(v1) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
119 |
val v2 = Node(node2); val l2 = levels(v2) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
120 |
if (l2 - l1 <= 1) (graph, levels) |
59263 | 121 |
else { |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
122 |
val dummies_levels = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
123 |
(for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
124 |
yield (Dummy(node1, node2, i), l)).toList |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
125 |
val dummies = dummies_levels.map(_._1) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
126 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
127 |
val levels1 = (levels /: dummies_levels)(_ + _) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
128 |
val graph1 = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
129 |
((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /: |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
130 |
(v1 :: dummies ::: List(v2)).sliding(2)) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
131 |
case (g, List(a, b)) => g.add_edge(a, b) } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
132 |
(graph1, levels1) |
59263 | 133 |
} |
134 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
135 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
136 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
137 |
/* minimize edge crossings and initial coordinates */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
138 |
|
50469 | 139 |
val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) |
140 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
141 |
val levels_graph: Graph = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
142 |
(((dummy_graph, 0.0) /: levels) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
143 |
case ((graph, y), level) => |
59312
c4b9b04bfc6d
proper level distance according to number of edges, as in old browser;
wenzelm
parents:
59311
diff
changeset
|
144 |
val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size } |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
145 |
((((graph, 0.0) /: level) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
146 |
case ((g, x), v) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
147 |
val w2 = metrics.box_width2(v) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
148 |
(g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap) |
59312
c4b9b04bfc6d
proper level distance according to number of edges, as in old browser;
wenzelm
parents:
59311
diff
changeset
|
149 |
})._1, y + metrics.box_height(num_edges)) |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
150 |
})._1 |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
151 |
|
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
152 |
|
59307 | 153 |
/* pendulum/rubberband layout */ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
154 |
|
59307 | 155 |
val output_graph = |
156 |
rubberband(metrics, levels, |
|
157 |
pendulum(metrics, levels, levels_graph)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
158 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
159 |
new Layout(metrics, input_graph, output_graph) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
} |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
162 |
|
49744 | 163 |
|
164 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
165 |
/** edge crossings **/ |
50469 | 166 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
167 |
private type Level = List[Vertex] |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
168 |
|
59307 | 169 |
private def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] = |
49745 | 170 |
{ |
59306 | 171 |
def resort(parent: Level, child: Level, top_down: Boolean): Level = |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
172 |
child.map(v => { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
173 |
val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) |
50469 | 174 |
val weight = |
50468 | 175 |
(0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
176 |
(v, weight) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
177 |
}).sortBy(_._2).map(_._1) |
50469 | 178 |
|
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
179 |
((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { |
59306 | 180 |
case ((old_levels, old_crossings, top_down), _) => |
181 |
val new_levels = |
|
182 |
if (top_down) |
|
183 |
(List(old_levels.head) /: old_levels.tail)((tops, bot) => |
|
184 |
resort(tops.head, bot, top_down) :: tops).reverse |
|
185 |
else { |
|
186 |
val rev_old_levels = old_levels.reverse |
|
187 |
(List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) => |
|
188 |
resort(bots.head, top, top_down) :: bots) |
|
189 |
} |
|
190 |
val new_crossings = count_crossings(graph, new_levels) |
|
191 |
if (new_crossings < old_crossings) |
|
192 |
(new_levels, new_crossings, !top_down) |
|
193 |
else |
|
194 |
(old_levels, old_crossings, !top_down) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
195 |
}._1 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
196 |
} |
50469 | 197 |
|
59307 | 198 |
private def level_list(levels: Levels): List[Level] = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
199 |
{ |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
200 |
val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
201 |
val buckets = new Array[Level](max_lev + 1) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
202 |
for (l <- 0 to max_lev) { buckets(l) = Nil } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
203 |
for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
204 |
buckets.iterator.map(_.sorted(Vertex.Ordering)).toList |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
205 |
} |
50469 | 206 |
|
59307 | 207 |
private def count_crossings(graph: Graph, levels: List[Level]): Int = |
59310 | 208 |
levels.iterator.sliding(2).map { |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
209 |
case List(top, bot) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
210 |
top.iterator.zipWithIndex.map { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
211 |
case (outer_parent, outer_parent_index) => |
59310 | 212 |
graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child => |
213 |
(0 until outer_parent_index).iterator.map(inner_parent => |
|
214 |
graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)). |
|
215 |
filter(inner_child => outer_child < inner_child).size).sum).sum |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
216 |
}.sum |
59310 | 217 |
}.sum |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
218 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
219 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
220 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
221 |
/** pendulum method **/ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
222 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
223 |
/*This is an auxiliary class which is used by the layout algorithm when |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
224 |
calculating coordinates with the "pendulum method". A "region" is a |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
225 |
group of vertices which "stick together".*/ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
226 |
private class Region(init: Vertex) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
227 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
228 |
var content: List[Vertex] = List(init) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
229 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
230 |
def distance(metrics: Metrics, graph: Graph, that: Region): Double = |
59307 | 231 |
vertex_left(metrics, graph, that.content.head) - |
232 |
vertex_right(metrics, graph, this.content.last) - |
|
233 |
metrics.box_gap |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
234 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
235 |
def deflection(graph: Graph, top_down: Boolean): Double = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
236 |
((for (a <- content.iterator) yield { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
237 |
val x = graph.get_node(a).x |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
238 |
val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
239 |
bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
240 |
}).sum / content.length).round.toDouble |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
241 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
242 |
def move(graph: Graph, dx: Double): Graph = |
59307 | 243 |
if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx)) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
244 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
245 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
246 |
private type Regions = List[List[Region]] |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
247 |
|
59307 | 248 |
private def pendulum(metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph = |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
249 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
250 |
def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
251 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
252 |
val (graph1, regions1, moved) = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
253 |
((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
254 |
case ((graph, tops, moved), bot) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
255 |
val bot1 = collapse(graph, bot, top_down) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
256 |
val (graph1, moved1) = deflect(graph, bot1, top_down) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
257 |
(graph1, bot1 :: tops, moved || moved1) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
258 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
259 |
(graph1, regions1.reverse, moved) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
260 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
261 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
262 |
def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] = |
50469 | 263 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
264 |
if (level.size <= 1) level |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
265 |
else { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
266 |
var next = level |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
267 |
var regions_changed = true |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
268 |
while (regions_changed) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
269 |
regions_changed = false |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
270 |
for (i <- Range(next.length - 1, 0, -1)) { |
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
271 |
val (r1, r2) = (next(i - 1), next(i)) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
272 |
val d1 = r1.deflection(graph, top_down) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
273 |
val d2 = r2.deflection(graph, top_down) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
274 |
|
50469 | 275 |
if (// Do regions touch? |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
276 |
r1.distance(metrics, graph, r2) <= 0.0 && |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
277 |
// Do they influence each other? |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
278 |
(d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
279 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
280 |
regions_changed = true |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
281 |
r1.content = r1.content ::: r2.content |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
282 |
next = next.filter(next.indexOf(_) != i) |
50469 | 283 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
284 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
285 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
286 |
next |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
287 |
} |
50469 | 288 |
} |
289 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
290 |
def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) = |
50469 | 291 |
{ |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
292 |
((graph, false) /: (0 until level.length)) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
293 |
case ((graph, moved), i) => |
59263 | 294 |
val r = level(i) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
295 |
val d = r.deflection(graph, top_down) |
59263 | 296 |
val offset = |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
297 |
if (d < 0 && i > 0) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
298 |
- (level(i - 1).distance(metrics, graph, r) min (- d)) |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
299 |
else if (d >= 0 && i < level.length - 1) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
300 |
r.distance(metrics, graph, level(i + 1)) min d |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
301 |
else d |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
302 |
(r.move(graph, offset), moved || d != 0) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
303 |
} |
50469 | 304 |
} |
305 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
306 |
val initial_regions = levels.map(level => level.map(new Region(_))) |
50469 | 307 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
308 |
((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
309 |
case ((graph, regions, top_down, moved), _) => |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
310 |
if (moved) { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
311 |
val (graph1, regions1, moved1) = iteration(graph, regions, top_down) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
312 |
(graph1, regions1, !top_down, moved1) |
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset
|
313 |
} |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
314 |
else (graph, regions, !top_down, moved) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
315 |
}._1 |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
316 |
} |
59307 | 317 |
|
318 |
||
319 |
||
320 |
/** rubberband method **/ |
|
321 |
||
322 |
private def force_weight(graph: Graph, v: Vertex): Double = |
|
323 |
{ |
|
324 |
val preds = graph.imm_preds(v) |
|
325 |
val succs = graph.imm_succs(v) |
|
326 |
val n = preds.size + succs.size |
|
327 |
if (n == 0) 0.0 |
|
328 |
else { |
|
329 |
val x = graph.get_node(v).x |
|
330 |
((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n |
|
331 |
} |
|
332 |
} |
|
333 |
||
334 |
private def rubberband(metrics: Metrics, levels: List[Level], graph: Graph): Graph = |
|
335 |
{ |
|
336 |
val gap = metrics.box_gap |
|
337 |
def left(g: Graph, v: Vertex) = vertex_left(metrics, g, v) |
|
338 |
def right(g: Graph, v: Vertex) = vertex_right(metrics, g, v) |
|
339 |
||
340 |
(graph /: (1 to rubberband_iterations)) { case (graph, _) => |
|
341 |
(graph /: levels) { case (graph, level) => |
|
342 |
val m = level.length - 1 |
|
343 |
(graph /: level.iterator.zipWithIndex) { |
|
344 |
case (g, (v, i)) => |
|
345 |
val d = force_weight(g, v) |
|
346 |
if (d < 0.0 && (i == 0 || right(g, level(i - 1)) + gap < left(g, v) + d) || |
|
347 |
d > 0.0 && (i == m || left(g, level(i + 1)) - gap > right(g, v) + d)) |
|
348 |
move_vertex(g, v, d.round.toDouble) |
|
349 |
else g |
|
350 |
} |
|
351 |
} |
|
352 |
} |
|
353 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
354 |
} |
59262 | 355 |
|
356 |
final class Layout private( |
|
59290 | 357 |
val metrics: Metrics, |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
358 |
val input_graph: Graph_Display.Graph, |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
359 |
val output_graph: Layout.Graph) |
59262 | 360 |
{ |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
361 |
/* vertex coordinates */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
362 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
363 |
def get_vertex(v: Layout.Vertex): Layout.Point = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
364 |
if (output_graph.defined(v)) output_graph.get_node(v) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
365 |
else Layout.Point.zero |
59290 | 366 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
367 |
def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
368 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
369 |
if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
370 |
else { |
59304 | 371 |
val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dx, p.y + dy)) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
372 |
new Layout(metrics, input_graph, output_graph1) |
59262 | 373 |
} |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
374 |
} |
59262 | 375 |
|
376 |
||
59290 | 377 |
/* dummies */ |
378 |
||
59292 | 379 |
def dummies_iterator: Iterator[Layout.Point] = |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
380 |
for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
381 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
382 |
def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
383 |
new Iterator[Layout.Point] { |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
384 |
private var index = 0 |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
385 |
def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index)) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
386 |
def next: Layout.Point = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
387 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
388 |
val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index)) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
389 |
index += 1 |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
390 |
p |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
391 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset
|
392 |
} |
59262 | 393 |
} |
394 |