equal
deleted
inserted
replaced
66 action = Action("Arrow Heads"){ |
66 action = Action("Arrow Heads"){ |
67 Parameters.arrow_heads = selected |
67 Parameters.arrow_heads = selected |
68 graph_panel.repaint() |
68 graph_panel.repaint() |
69 } |
69 } |
70 } |
70 } |
71 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
72 contents += new CheckBox(){ |
|
73 selected = Parameters.long_names |
|
74 action = Action("Long Names"){ |
|
75 Parameters.long_names = selected |
|
76 graph_panel.repaint() |
|
77 } |
|
78 } |
|
79 contents += Swing.RigidBox(new Dimension(10, 0)) |
71 contents += Swing.RigidBox(new Dimension(10, 0)) |
80 contents += new Button{ |
72 contents += new Button{ |
81 action = Action("Save as PNG"){ |
73 action = Action("Save as PNG"){ |
82 chooser.showSaveDialog(this) match { |
74 chooser.showSaveDialog(this) match { |
83 case FileChooser.Result.Approve => { |
75 case FileChooser.Result.Approve => { |