equal
deleted
inserted
replaced
61 def fit_to_window() = { |
61 def fit_to_window() = { |
62 Transform.fit_to_window() |
62 Transform.fit_to_window() |
63 refresh() |
63 refresh() |
64 } |
64 } |
65 |
65 |
66 val zoom_box: GUI.Zoom_Box = new GUI.Zoom_Box(percent => rescale(0.01 * percent)) |
66 val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } |
67 |
67 |
68 def rescale(s: Double) |
68 def rescale(s: Double) |
69 { |
69 { |
70 Transform.scale = s |
70 Transform.scale = s |
71 if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt) |
71 if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt) |
72 refresh() |
72 refresh() |
73 } |
73 } |
74 |
74 |
75 def apply_layout() = visualizer.Coordinates.update_layout() |
75 def apply_layout() = visualizer.Coordinates.update_layout() |
76 |
76 |