diff options
| -rw-r--r-- | unit_trace/viz/viewer.py | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/unit_trace/viz/viewer.py b/unit_trace/viz/viewer.py index 5e707b8..fb31e8a 100644 --- a/unit_trace/viz/viewer.py +++ b/unit_trace/viz/viewer.py | |||
| @@ -116,21 +116,21 @@ class GraphArea(gtk.DrawingArea): | |||
| 116 | 116 | ||
| 117 | def get_schedule(self): | 117 | def get_schedule(self): |
| 118 | return self.renderer.get_schedule() | 118 | return self.renderer.get_schedule() |
| 119 | 119 | ||
| 120 | def zoom_in(self): | 120 | def zoom_in(self): |
| 121 | scale = self.scale + GraphArea.ZOOM_INCR | 121 | scale = self.scale + GraphArea.ZOOM_INCR |
| 122 | if scale > GraphArea.MAX_ZOOM_IN: | 122 | if scale > GraphArea.MAX_ZOOM_IN: |
| 123 | scale = GraphArea.MAX_ZOOM_IN | 123 | scale = GraphArea.MAX_ZOOM_IN |
| 124 | self.set_scale(scale) | 124 | self.set_scale(scale) |
| 125 | self.config_scrollbars(self.cur_x, self.cur_y, self.scale) | 125 | self.config_scrollbars(self.cur_x, self.cur_y, self.scale) |
| 126 | 126 | ||
| 127 | def zoom_out(self): | 127 | def zoom_out(self): |
| 128 | scale = self.scale - GraphArea.ZOOM_INCR | 128 | scale = self.scale - GraphArea.ZOOM_INCR |
| 129 | if scale < GraphArea.MIN_ZOOM_OUT: | 129 | if scale < GraphArea.MIN_ZOOM_OUT: |
| 130 | scale = GraphArea.MIN_ZOOM_OUT | 130 | scale = GraphArea.MIN_ZOOM_OUT |
| 131 | self.set_scale(scale) | 131 | self.set_scale(scale) |
| 132 | self.config_scrollbars(self.cur_x, self.cur_y, self.scale) | 132 | self.config_scrollbars(self.cur_x, self.cur_y, self.scale) |
| 133 | 133 | ||
| 134 | def set_scale(self, scale): | 134 | def set_scale(self, scale): |
| 135 | if scale == self.scale: | 135 | if scale == self.scale: |
| 136 | return | 136 | return |
| @@ -145,7 +145,7 @@ class GraphArea(gtk.DrawingArea): | |||
| 145 | value = max(value, self.horizontal.get_lower()) | 145 | value = max(value, self.horizontal.get_lower()) |
| 146 | value = min(value, self.horizontal.get_upper() - self.horizontal.get_page_size()) | 146 | value = min(value, self.horizontal.get_upper() - self.horizontal.get_page_size()) |
| 147 | self.horizontal.set_value(value) | 147 | self.horizontal.set_value(value) |
| 148 | 148 | ||
| 149 | def set_vvalue(self, value): | 149 | def set_vvalue(self, value): |
| 150 | if self.vertical is None: | 150 | if self.vertical is None: |
| 151 | return | 151 | return |
| @@ -153,7 +153,7 @@ class GraphArea(gtk.DrawingArea): | |||
| 153 | value = max(value, self.vertical.get_lower()) | 153 | value = max(value, self.vertical.get_lower()) |
| 154 | value = min(value, self.vertical.get_upper() - self.vertical.get_page_size()) | 154 | value = min(value, self.vertical.get_upper() - self.vertical.get_page_size()) |
| 155 | self.vertical.set_value(value) | 155 | self.vertical.set_value(value) |
| 156 | 156 | ||
| 157 | def set_scroll_adjustments(self, widget, horizontal, vertical, data=None): | 157 | def set_scroll_adjustments(self, widget, horizontal, vertical, data=None): |
| 158 | graph = self.renderer.get_graph() | 158 | graph = self.renderer.get_graph() |
| 159 | width = graph.get_width() | 159 | width = graph.get_width() |
| @@ -204,7 +204,7 @@ class GraphArea(gtk.DrawingArea): | |||
| 204 | graph.get_attrs().y_item_size * GraphArea.VERT_PAGE_SCROLL_FACTOR / scale, | 204 | graph.get_attrs().y_item_size * GraphArea.VERT_PAGE_SCROLL_FACTOR / scale, |
| 205 | self.height / scale) | 205 | self.height / scale) |
| 206 | self.set_vvalue(vvalue) | 206 | self.set_vvalue(vvalue) |
| 207 | 207 | ||
| 208 | def refresh_events(self, sender, new, old, replace): | 208 | def refresh_events(self, sender, new, old, replace): |
| 209 | """Even if the selected areas change on one graph, they change | 209 | """Even if the selected areas change on one graph, they change |
| 210 | everywhere, and different events might be in different regions on | 210 | everywhere, and different events might be in different regions on |
