clarified fit_to_window: floor scale within window bounds;

--- a/src/Tools/Graphview/graph_panel.scala	Sat Jan 03 21:50:50 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sat Jan 03 22:04:31 2015 +0100
@@ -70,7 +70,7 @@
   def rescale(s: Double)
   {
     Transform.scale = s
-    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt)
+    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
     refresh()
   }
 
@@ -130,8 +130,9 @@
     {
       _scale = (s min 10.0) max 0.1
     }
+
     def scale_discrete: Double =
-      (_scale * visualizer.font_size).round.toDouble / visualizer.font_size
+      (scale * visualizer.font_size).floor / visualizer.font_size
 
     def apply() =
     {

--- a/src/Tools/Graphview/main_panel.scala	Sat Jan 03 21:50:50 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Sat Jan 03 22:04:31 2015 +0100
@@ -54,8 +54,8 @@
         }
       },
       graph_panel.zoom,
+      new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
       new Button { action = Action("Apply layout") { graph_panel.apply_layout() } },
-      new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
       new Button { action = Action("Colorations") { color_dialog.open } },
       new Button { action = Action("Filters") { mutator_dialog.open } })
 

--- a/src/Tools/Graphview/popups.scala	Sat Jan 03 21:50:50 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Sat Jan 03 22:04:31 2015 +0100
@@ -142,8 +142,7 @@
       popup.add(new JPopupMenu.Separator)
     }
 
-    popup.add(
-      new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer)
+    popup.add(new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer)
 
     popup
   }