equal
deleted
inserted
replaced
41 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
41 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
42 new CheckBox() { |
42 new CheckBox() { |
43 selected = visualizer.arrow_heads |
43 selected = visualizer.arrow_heads |
44 action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() } |
44 action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() } |
45 }, |
45 }, |
|
46 new CheckBox() { |
|
47 selected = visualizer.show_dummies |
|
48 action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() } |
|
49 }, |
46 new Button { |
50 new Button { |
47 action = Action("Save image") { |
51 action = Action("Save image") { |
48 chooser.showSaveDialog(this) match { |
52 chooser.showSaveDialog(this) match { |
49 case FileChooser.Result.Approve => export(chooser.selectedFile) |
53 case FileChooser.Result.Approve => export(chooser.selectedFile) |
50 case _ => |
54 case _ => |
69 def paint(gfx: Graphics2D) |
73 def paint(gfx: Graphics2D) |
70 { |
74 { |
71 gfx.setColor(Color.WHITE) |
75 gfx.setColor(Color.WHITE) |
72 gfx.fillRect(0, 0, w, h) |
76 gfx.fillRect(0, 0, w, h) |
73 gfx.translate(- box.x, - box.y) |
77 gfx.translate(- box.x, - box.y) |
74 visualizer.Drawer.paint_all_visible(gfx, false) |
78 visualizer.paint_all_visible(gfx) |
75 } |
79 } |
76 |
80 |
77 try { |
81 try { |
78 val name = file.getName |
82 val name = file.getName |
79 if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
83 if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |