equal
deleted
inserted
replaced
143 reposition(d, (x + dx, y + dy)) |
143 reposition(d, (x + dx, y + dy)) |
144 } |
144 } |
145 |
145 |
146 def update_layout() |
146 def update_layout() |
147 { |
147 { |
148 val m = metrics() |
|
149 val visible_graph = model.make_visible_graph() |
|
150 |
|
151 val max_width = |
|
152 visible_graph.keys_iterator.map(node => m.string_bounds(node.toString).getWidth).max |
|
153 val box_distance = (max_width + m.pad + m.gap).ceil |
|
154 def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil |
|
155 |
|
156 // FIXME avoid expensive operation on GUI thread |
148 // FIXME avoid expensive operation on GUI thread |
157 layout = Layout.make(visible_graph, box_distance, box_height _) |
149 layout = Layout.make(metrics(), model.make_visible_graph()) |
158 } |
150 } |
159 |
151 |
160 def bounding_box(): Rectangle2D.Double = |
152 def bounding_box(): Rectangle2D.Double = |
161 { |
153 { |
162 val m = metrics() |
154 val m = metrics() |