equal
deleted
inserted
replaced
3663 self.RefreshScrollBars() |
3663 self.RefreshScrollBars() |
3664 event.Skip() |
3664 event.Skip() |
3665 |
3665 |
3666 def OnMouseWheelWindow(self, event): |
3666 def OnMouseWheelWindow(self, event): |
3667 if self.StartMousePos is None or self.StartScreenPos is None: |
3667 if self.StartMousePos is None or self.StartScreenPos is None: |
3668 rotation = event.GetWheelRotation() / event.GetWheelDelta() |
3668 rotation = event.GetWheelRotation() // event.GetWheelDelta() |
3669 if event.ShiftDown(): |
3669 if event.ShiftDown(): |
3670 x, y = self.GetViewStart() |
3670 x, y = self.GetViewStart() |
3671 xp = max(0, min(x - rotation * 3, self.Editor.GetVirtualSize()[0] / self.Editor.GetScrollPixelsPerUnit()[0])) |
3671 xp = max(0, min(x - rotation * 3, self.Editor.GetVirtualSize()[0] / self.Editor.GetScrollPixelsPerUnit()[0])) |
3672 self.RefreshVisibleElements(xp=xp) |
3672 self.RefreshVisibleElements(xp=xp) |
3673 self.Scroll(xp, y) |
3673 self.Scroll(xp, y) |