equal
deleted
inserted
replaced
60 def fit_to_window() = { |
60 def fit_to_window() = { |
61 Transform.fit_to_window() |
61 Transform.fit_to_window() |
62 refresh() |
62 refresh() |
63 } |
63 } |
64 |
64 |
65 val zoom_box: Library.Zoom_Box = |
65 val zoom_box: GUI.Zoom_Box = new GUI.Zoom_Box(percent => rescale(0.01 * percent)) |
66 new Library.Zoom_Box(percent => rescale(0.01 * percent)) |
|
67 |
66 |
68 def rescale(s: Double) |
67 def rescale(s: Double) |
69 { |
68 { |
70 Transform.scale = s |
69 Transform.scale = s |
71 if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt) |
70 if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt) |