equal
deleted
inserted
replaced
64 add(graph_panel, BorderPanel.Position.Center) |
64 add(graph_panel, BorderPanel.Position.Center) |
65 add(options_panel, BorderPanel.Position.North) |
65 add(options_panel, BorderPanel.Position.North) |
66 |
66 |
67 private def export(file: JFile) |
67 private def export(file: JFile) |
68 { |
68 { |
69 val box = visualizer.Coordinates.bounding_box() |
69 val box = visualizer.bounding_box() |
70 val w = box.width.ceil.toInt |
70 val w = box.width.ceil.toInt |
71 val h = box.height.ceil.toInt |
71 val h = box.height.ceil.toInt |
72 |
72 |
73 def paint(gfx: Graphics2D) |
73 def paint(gfx: Graphics2D) |
74 { |
74 { |