equal
deleted
inserted
replaced
110 { |
110 { |
111 var x0 = 0.0 |
111 var x0 = 0.0 |
112 var y0 = 0.0 |
112 var y0 = 0.0 |
113 var x1 = 0.0 |
113 var x1 = 0.0 |
114 var y1 = 0.0 |
114 var y1 = 0.0 |
115 for (node <- visible_graph.keys_iterator) { |
115 ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++ |
116 val shape = Shapes.Node.shape(visualizer, node) |
116 (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))). |
117 x0 = x0 min shape.getMinX |
117 foreach(rect => { |
118 y0 = y0 min shape.getMinY |
118 x0 = x0 min rect.getMinX |
119 x1 = x1 max shape.getMaxX |
119 y0 = y0 min rect.getMinY |
120 y1 = y1 max shape.getMaxY |
120 x1 = x1 max rect.getMaxX |
121 } |
121 y1 = y1 max rect.getMaxY |
|
122 }) |
122 val gap = metrics.gap |
123 val gap = metrics.gap |
123 x0 = (x0 - gap).floor |
124 x0 = (x0 - gap).floor |
124 y0 = (y0 - gap).floor |
125 y0 = (y0 - gap).floor |
125 x1 = (x1 + gap).ceil |
126 x1 = (x1 + gap).ceil |
126 y1 = (y1 + gap).ceil |
127 y1 = (y1 + gap).ceil |