author  wenzelm 
Tue, 06 Jan 2015 16:43:17 +0100  
changeset 59304  848e27e4ac37 
parent 59302  4d985afc0565 
child 59305  b5e33012180e 
permissions  rwrr 
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 

59261  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/3540589503_371 

11 
ftp://ftp.cs.unisb.de/pub/graphics/vcg/doc/trA0394.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, _: Dummy) => 1 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

31 
case (_: Dummy, _: Node) => 1 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

32 
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

33 
case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

34 
Graph_Display.Node.Ordering.compare(a1, b1) match { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

35 
case 0 => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

36 
Graph_Display.Node.Ordering.compare(a2, b2) match { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

37 
case 0 => i compare j 
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 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

40 
case ord => ord 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

41 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

42 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

43 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

44 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

45 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

46 
sealed abstract class Vertex 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

47 
case class Node(node: Graph_Display.Node) extends Vertex 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

48 
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

49 

59262  50 
object Point { val zero: Point = Point(0.0, 0.0) } 
51 
case class Point(x: Double, y: Double) 

50469  52 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

53 
type Graph = isabelle.Graph[Vertex, Point] 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

54 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

55 
def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

56 
isabelle.Graph.make(entries)(Vertex.Ordering) 
59262  57 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

58 
val empty_graph: Graph = make_graph(Nil) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

59 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

60 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

61 
/* layout */ 
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 
val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) 
50470  64 

49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

65 
val pendulum_iterations = 10 
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset

66 
val minimize_crossings_iterations = 40 
50469  67 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

68 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

69 
private type Levels = Map[Vertex, Int] 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

70 
private val empty_levels: Levels = Map.empty 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

71 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

72 
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

73 
{ 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

74 
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

75 
else { 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

76 
/* initial graph */ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

77 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

78 
val initial_graph = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

79 
make_graph( 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

80 
input_graph.iterator.map( 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

81 
{ 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

82 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

83 
val initial_levels: Levels = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

84 
(empty_levels /: initial_graph.topological_order) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

85 
case (levels, vertex) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

86 
val level = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

87 
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

88 
levels + (vertex > level) 
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 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

91 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

92 
/* graph with dummies */ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

93 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

94 
val (dummy_graph, dummy_levels) = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

95 
((initial_graph, initial_levels) /: input_graph.edges_iterator) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

96 
case ((graph, levels), (node1, node2)) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

97 
val v1 = Node(node1); val l1 = levels(v1) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

98 
val v2 = Node(node2); val l2 = levels(v2) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

99 
if (l2  l1 <= 1) (graph, levels) 
59263  100 
else { 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

101 
val dummies_levels = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

102 
(for { (l, i) < ((l1 + 1) until l2).iterator.zipWithIndex } 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

103 
yield (Dummy(node1, node2, i), l)).toList 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

104 
val dummies = dummies_levels.map(_._1) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

105 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

106 
val levels1 = (levels /: dummies_levels)(_ + _) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

107 
val graph1 = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

108 
((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /: 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

109 
(v1 :: dummies ::: List(v2)).sliding(2)) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

110 
case (g, List(a, b)) => g.add_edge(a, b) } 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

111 
(graph1, levels1) 
59263  112 
} 
113 
} 

49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

114 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

115 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

116 
/* minimize edge crossings and initial coordinates */ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

117 

50469  118 
val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) 
119 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

120 
val levels_graph: Graph = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

121 
(((dummy_graph, 0.0) /: levels) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

122 
case ((graph, y), level) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

123 
((((graph, 0.0) /: level) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

124 
case ((g, x), v) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

125 
val w2 = metrics.box_width2(v) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

126 
(g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap) 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

127 
})._1, y + metrics.box_height(level.length)) 
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset

128 
})._1 
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset

129 

59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

130 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

131 
/* pendulum layout */ 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

132 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

133 
val output_graph = pendulum(metrics, levels_graph, levels) 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

134 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

135 
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

136 
} 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

137 
} 
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset

138 

49744  139 

140 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

141 
/** edge crossings **/ 
50469  142 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

143 
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

144 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

145 
def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] = 
49745  146 
{ 
50469  147 
def resort_level(parent: Level, child: Level, top_down: Boolean): Level = 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

148 
child.map(v => { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

149 
val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) 
50469  150 
val weight = 
50468  151 
(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

152 
(v, weight) 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

153 
}).sortBy(_._2).map(_._1) 
50469  154 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

155 
def resort(levels: List[Level], top_down: Boolean) = 
59263  156 
if (top_down) 
157 
(List(levels.head) /: levels.tail)((tops, bot) => 

158 
resort_level(tops.head, bot, top_down) :: tops).reverse 

159 
else { 

160 
val rev_levels = levels.reverse 

161 
(List(rev_levels.head) /: rev_levels.tail)((bots, top) => 

162 
resort_level(bots.head, top, top_down) :: bots) 

49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

163 
} 
50469  164 

49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset

165 
((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

166 
case ((old_levels, old_crossings, top_down), _) => { 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

167 
val new_levels = resort(old_levels, top_down) 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

168 
val new_crossings = count_crossings(graph, new_levels) 
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset

169 
if (new_crossings < old_crossings) 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

170 
(new_levels, new_crossings, !top_down) 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

171 
else 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

172 
(old_levels, old_crossings, !top_down) 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

173 
} 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

174 
}._1 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

175 
} 
50469  176 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

177 
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

178 
{ 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

179 
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

180 
val buckets = new Array[Level](max_lev + 1) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

181 
for (l < 0 to max_lev) { buckets(l) = Nil } 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

182 
for ((v, l) < levels) { buckets(l) = v :: buckets(l) } 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

183 
buckets.iterator.map(_.sorted(Vertex.Ordering)).toList 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

184 
} 
50469  185 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

186 
def count_crossings(graph: Graph, levels: List[Level]): Int = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

187 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

188 
def in_level(ls: List[Level]): Int = ls match { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

189 
case List(top, bot) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

190 
top.iterator.zipWithIndex.map { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

191 
case (outer_parent, outer_parent_index) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

192 
graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

193 
.map(outer_child => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

194 
(0 until outer_parent_index) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

195 
.map(inner_parent => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

196 
graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

197 
.filter(inner_child => outer_child < inner_child) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

198 
.size 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

199 
).sum 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

200 
).sum 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

201 
}.sum 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

202 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

203 
case _ => 0 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

204 
} 
50469  205 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

206 
levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

207 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

208 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

209 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

210 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

211 
/** pendulum method **/ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

212 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

213 
/*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

214 
calculating coordinates with the "pendulum method". A "region" is a 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

215 
group of vertices which "stick together".*/ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

216 
private class Region(init: Vertex) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

217 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

218 
var content: List[Vertex] = List(init) 
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 
def distance(metrics: Metrics, graph: Graph, that: Region): Double = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

221 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

222 
val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

223 
val v2 = that.content.head; val x2 = graph.get_node(v2).x  metrics.box_width2(v2) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

224 
x2  x1  metrics.box_gap 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

225 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

226 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

227 
def deflection(graph: Graph, top_down: Boolean): Double = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

228 
((for (a < content.iterator) yield { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

229 
val x = graph.get_node(a).x 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

230 
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

231 
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

232 
}).sum / content.length).round.toDouble 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

233 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

234 
def move(graph: Graph, dx: Double): Graph = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

235 
if (dx == 0.0) graph 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

236 
else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) } 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

237 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

238 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

239 
private type Regions = List[List[Region]] 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

240 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

241 
def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

242 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

243 
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

244 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

245 
val (graph1, regions1, moved) = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

246 
((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

247 
case ((graph, tops, moved), bot) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

248 
val bot1 = collapse(graph, bot, top_down) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

249 
val (graph1, moved1) = deflect(graph, bot1, top_down) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

250 
(graph1, bot1 :: tops, moved  moved1) 
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 
(graph1, regions1.reverse, moved) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

253 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

254 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

255 
def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] = 
50469  256 
{ 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

257 
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

258 
else { 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

259 
var next = level 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

260 
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

261 
while (regions_changed) { 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

262 
regions_changed = false 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

263 
for (i < Range(next.length  1, 0, 1)) { 
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

264 
val (r1, r2) = (next(i  1), next(i)) 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

265 
val d1 = r1.deflection(graph, top_down) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

266 
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

267 

50469  268 
if (// Do regions touch? 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

269 
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

270 
// Do they influence each other? 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

271 
(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

272 
{ 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

273 
regions_changed = true 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

274 
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

275 
next = next.filter(next.indexOf(_) != i) 
50469  276 
} 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

277 
} 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

278 
} 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

279 
next 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

280 
} 
50469  281 
} 
282 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

283 
def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) = 
50469  284 
{ 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

285 
((graph, false) /: (0 until level.length)) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

286 
case ((graph, moved), i) => 
59263  287 
val r = level(i) 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

288 
val d = r.deflection(graph, top_down) 
59263  289 
val offset = 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

290 
if (d < 0 && i > 0) 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

291 
 (level(i  1).distance(metrics, graph, r) min ( d)) 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

292 
else if (d >= 0 && i < level.length  1) 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

293 
r.distance(metrics, graph, level(i + 1)) min d 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

294 
else d 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

295 
(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

296 
} 
50469  297 
} 
298 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

299 
val initial_regions = levels.map(level => level.map(new Region(_))) 
50469  300 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

301 
((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

302 
case ((graph, regions, top_down, moved), _) => 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

303 
if (moved) { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

304 
val (graph1, regions1, moved1) = iteration(graph, regions, top_down) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

305 
(graph1, regions1, !top_down, moved1) 
59265
962ad3942ea7
more metrics, with integer coordinates for layout;
wenzelm
parents:
59264
diff
changeset

306 
} 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

307 
else (graph, regions, !top_down, moved) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

308 
}._1 
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

309 
} 
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset

310 
} 
59262  311 

312 
final class Layout private( 

59290  313 
val metrics: Metrics, 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

314 
val input_graph: Graph_Display.Graph, 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

315 
val output_graph: Layout.Graph) 
59262  316 
{ 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

317 
/* vertex coordinates */ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

318 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

319 
def get_vertex(v: Layout.Vertex): Layout.Point = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

320 
if (output_graph.defined(v)) output_graph.get_node(v) 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

321 
else Layout.Point.zero 
59290  322 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

323 
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

324 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

325 
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

326 
else { 
59304  327 
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

328 
new Layout(metrics, input_graph, output_graph1) 
59262  329 
} 
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

330 
} 
59262  331 

332 

59290  333 
/* dummies */ 
334 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

335 
def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

336 
output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d }) 
59292  337 

338 
def dummies_iterator: Iterator[Layout.Point] = 

59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

339 
for ((_: Layout.Dummy, (p, _)) < output_graph.iterator) yield p 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

340 

4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

341 
def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

342 
new Iterator[Layout.Point] { 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

343 
private var index = 0 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

344 
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

345 
def next: Layout.Point = 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

346 
{ 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

347 
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

348 
index += 1 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

349 
p 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

350 
} 
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59292
diff
changeset

351 
} 
59262  352 
} 
353 