equal
deleted
inserted
replaced
65 x1 = (x1 + metrics.gap).ceil |
65 x1 = (x1 + metrics.gap).ceil |
66 y1 = (y1 + metrics.gap).ceil |
66 y1 = (y1 + metrics.gap).ceil |
67 new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) |
67 new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) |
68 } |
68 } |
69 |
69 |
70 def update_layout() |
70 def update_layout(): Unit = |
71 { |
71 { |
72 val metrics = Metrics(make_font()) |
72 val metrics = Metrics(make_font()) |
73 val visible_graph = model.make_visible_graph() |
73 val visible_graph = model.make_visible_graph() |
74 |
74 |
75 def node_text(node: Graph_Display.Node, content: XML.Body): String = |
75 def node_text(node: Graph_Display.Node, content: XML.Body): String = |
137 curr = (curr + 1) % filter_colors.length |
137 curr = (curr + 1) % filter_colors.length |
138 filter_colors(curr) |
138 filter_colors(curr) |
139 } |
139 } |
140 } |
140 } |
141 |
141 |
142 def paint(gfx: Graphics2D) |
142 def paint(gfx: Graphics2D): Unit = |
143 { |
143 { |
144 gfx.setRenderingHints(Metrics.rendering_hints) |
144 gfx.setRenderingHints(Metrics.rendering_hints) |
145 |
145 |
146 for (node <- graphview.current_node) |
146 for (node <- graphview.current_node) |
147 Shapes.highlight_node(gfx, graphview, node) |
147 Shapes.highlight_node(gfx, graphview, node) |