changeset 50478 | ccfdd1f6cf10 |
parent 50475 | 8cc351df4a23 |
child 50491 | 0faaa279faee |
--- a/src/Tools/Graphview/src/main_panel.scala Tue Dec 11 21:55:56 2012 +0100 +++ b/src/Tools/Graphview/src/main_panel.scala Tue Dec 11 22:09:22 2012 +0100 @@ -71,6 +71,9 @@ } } contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Library.Zoom_Box(percent => graph_panel.rescale(0.01 * percent)) + + contents += Swing.RigidBox(new Dimension(10, 0)) contents += new Button{ action = Action("Apply Layout"){ graph_panel.apply_layout()