# HG changeset patch
# User wenzelm
# Date 1355320488 -3600
# Node ID 0faaa279faee2eaf02b29b8ef92a2b4714cfabf7
# Parent  b977b727c7d58cfd7f0d87217dc6738a3296c7f7
improved coupling of zoom_box and scale;
explicit rescale(1.0) on startup;

diff -r b977b727c7d5 -r 0faaa279faee src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Dec 12 13:28:23 2012 +0100
+++ b/src/Pure/library.scala	Wed Dec 12 14:54:48 2012 +0100
@@ -178,8 +178,16 @@
           if (10 <= i && i <= 1000) i else 100
         case _ => 100
       }
+
     def print(i: Int): String = i.toString + "%"
 
+    def set_item(i: Int) {
+      peer.getEditor match {
+        case null =>
+        case editor => editor.setItem(print(i))
+      }
+    }
+
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
     reactions += {
       case SelectionChanged(_) => apply_factor(parse(selection.item))
diff -r b977b727c7d5 -r 0faaa279faee src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Wed Dec 12 13:28:23 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala	Wed Dec 12 14:54:48 2012 +0100
@@ -51,8 +51,10 @@
 
   def refresh()
   {
-    paint_panel.set_preferred_size()
-    paint_panel.repaint()
+    if (paint_panel != null) {
+      paint_panel.set_preferred_size()
+      paint_panel.repaint()
+    }
   }
 
   def fit_to_window() = {
@@ -60,9 +62,13 @@
     refresh()
   }
 
+  val zoom_box: Library.Zoom_Box =
+    new Library.Zoom_Box(percent => rescale(0.01 * percent))
+
   def rescale(s: Double)
   {
     Transform.scale = s
+    if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt)
     refresh()
   }
 
@@ -109,7 +115,7 @@
   visualizer.model.Mutators.events += { case _ => repaint() }
 
   apply_layout()
-  fit_to_window()
+  rescale(1.0)
 
   private object Transform
   {
@@ -120,7 +126,6 @@
     def scale_=(s: Double)
     {
       _scale = (s min 10) max 0.1
-      paint_panel.set_preferred_size()
     }
     def scale_discrete: Double =
       (_scale * visualizer.font_size).round.toDouble / visualizer.font_size
@@ -135,13 +140,13 @@
 
     def fit_to_window() {
       if (visualizer.model.visible_nodes().isEmpty)
-        scale = 1
+        rescale(1.0)
       else {
         val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
 
         val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
         val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
-        scale = sx min sy
+        rescale(sx min sy)
       }
     }
 
@@ -164,8 +169,8 @@
 
       def typed(c: Char, m: Modifiers) =
         (c, m) match {
-          case ('+', _) => Transform.scale *= 5.0/4
-          case ('-', _) => Transform.scale *= 4.0/5
+          case ('+', _) => rescale(Transform.scale * 5.0/4)
+          case ('-', _) => rescale(Transform.scale * 4.0/5)
           case ('0', _) => Transform.fit_to_window()
           case ('1', _) => visualizer.Coordinates.update_layout()
           case ('2', _) => Transform.fit_to_window()
@@ -275,7 +280,7 @@
       def wheel(rotation: Int, at: Point) {
         val at2 = Transform.pane_to_graph_coordinates(at)
         // > 0 -> up
-        Transform.scale *= (if (rotation > 0) 4.0/5 else 5.0/4)
+        rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4))
 
         // move mouseposition to center
         Transform().transform(at2, at2)
diff -r b977b727c7d5 -r 0faaa279faee src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Wed Dec 12 13:28:23 2012 +0100
+++ b/src/Tools/Graphview/src/main_panel.scala	Wed Dec 12 14:54:48 2012 +0100
@@ -71,7 +71,7 @@
       }
     }
     contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Library.Zoom_Box(percent => graph_panel.rescale(0.01 * percent))
+    contents += graph_panel.zoom_box
 
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += new Button{