equal
deleted
inserted
replaced
1 /* Title: Tools/Graphview/layout.scala |
1 /* Title: Tools/Graphview/layout.scala |
2 Author: Markus Kaiser, TU Muenchen |
2 Author: Markus Kaiser, TU Muenchen |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Pendulum DAG layout algorithm. |
5 DAG layout algorithm, according to: |
|
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 |
6 */ |
12 */ |
7 |
13 |
8 package isabelle.graphview |
14 package isabelle.graphview |
9 |
15 |
10 |
16 |
259 } |
265 } |
260 else (regions, coords, !top_down, moved) |
266 else (regions, coords, !top_down, moved) |
261 }._2 |
267 }._2 |
262 } |
268 } |
263 |
269 |
|
270 /*This is an auxiliary class which is used by the layout algorithm when |
|
271 calculating coordinates with the "pendulum method". A "region" is a |
|
272 group of nodes which "stick together".*/ |
264 private class Region(val graph: Graph_Display.Graph, node: Key) |
273 private class Region(val graph: Graph_Display.Graph, node: Key) |
265 { |
274 { |
266 var nodes: List[Key] = List(node) |
275 var nodes: List[Key] = List(node) |
267 |
276 |
268 def left(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).min |
277 def left(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).min |