added explicit zoom box;

--- a/src/Tools/Graphview/src/graph_panel.scala	Tue Dec 11 21:55:56 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala	Tue Dec 11 22:09:22 2012 +0100
@@ -60,6 +60,12 @@
     refresh()
   }
 
+  def rescale(s: Double)
+  {
+    Transform.scale = s
+    refresh()
+  }
+
   def apply_layout() = visualizer.Coordinates.update_layout()
 
   private class Paint_Panel extends Panel {

--- 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()