diff -r ffa18243a4e3 -r ccfdd1f6cf10 src/Tools/Graphview/src/main_panel.scala
--- 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()