src/Tools/Graphview/src/main_panel.scala

           case _ =>
         }
       }
     }
     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()
       }
     }