# HG changeset patch
# User wenzelm
# Date 1355260162 -3600
# Node ID ccfdd1f6cf10ee4bbbf2b0fe5b2cab37306361a7
# Parent  ffa18243a4e3266584db5ff6bbfb794d2fc96891
added explicit zoom box;

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