equal
deleted
inserted
replaced
743 self.Editor.Bind(wx.EVT_SCROLLWIN_THUMBRELEASE, self.OnScrollStop) |
743 self.Editor.Bind(wx.EVT_SCROLLWIN_THUMBRELEASE, self.OnScrollStop) |
744 self.Editor.Bind(wx.EVT_MOUSEWHEEL, self.OnMouseWheelWindow) |
744 self.Editor.Bind(wx.EVT_MOUSEWHEEL, self.OnMouseWheelWindow) |
745 self.Editor.Bind(wx.EVT_SIZE, self.OnMoveWindow) |
745 self.Editor.Bind(wx.EVT_SIZE, self.OnMoveWindow) |
746 self.Editor.Bind(wx.EVT_MOUSE_EVENTS, self.OnViewerMouseEvent) |
746 self.Editor.Bind(wx.EVT_MOUSE_EVENTS, self.OnViewerMouseEvent) |
747 |
747 |
748 # Destructor |
|
749 def __del__(self): |
|
750 DebugViewer.__del__(self) |
|
751 self.Flush() |
|
752 self.ResetView() |
|
753 self.RefreshHighlightsTimer.Stop() |
|
754 |
|
755 def SetCurrentCursor(self, cursor): |
748 def SetCurrentCursor(self, cursor): |
756 if self.Mode != MODE_MOTION: |
749 if self.Mode != MODE_MOTION: |
757 if self.CurrentCursor != cursor: |
750 if self.CurrentCursor != cursor: |
758 self.CurrentCursor = cursor |
751 self.CurrentCursor = cursor |
759 self.Editor.SetCursor(CURSORS[cursor]) |
752 self.Editor.SetCursor(CURSORS[cursor]) |