--- a/src/Tools/Graphview/graph_panel.scala Sun Jan 18 22:03:53 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 18 22:07:45 2015 +0100
@@ -100,12 +100,6 @@
}
}
- def fit_to_window()
- {
- Transform.fit_to_window()
- refresh()
- }
-
val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
def rescale(s: Double)
@@ -120,6 +114,12 @@
/* transform */
+ def fit_to_window()
+ {
+ Transform.fit_to_window()
+ refresh()
+ }
+
private object Transform
{
private var _scale: Double = 1.0
@@ -166,6 +166,9 @@
/* interaction */
+ visualizer.model.Colors.events += { case _ => repaint() }
+ visualizer.model.Mutators.events += { case _ => repaint() }
+
listenTo(mouse.moves)
listenTo(mouse.clicks)
reactions +=
@@ -181,9 +184,6 @@
repaint()
}
- visualizer.model.Colors.events += { case _ => repaint() }
- visualizer.model.Mutators.events += { case _ => repaint() }
-
private object Mouse_Interaction
{
private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =