equal
deleted
inserted
replaced
615 |
615 |
616 # Refresh the current scaling |
616 # Refresh the current scaling |
617 def RefreshScaling(self, refresh=True): |
617 def RefreshScaling(self, refresh=True): |
618 properties = self.Controler.GetProjectProperties(self.Debug) |
618 properties = self.Controler.GetProjectProperties(self.Debug) |
619 scaling = properties["scaling"][self.CurrentLanguage] |
619 scaling = properties["scaling"][self.CurrentLanguage] |
620 if scaling != (0, 0): |
620 if scaling[0] != 0 and scaling[1] != 0: |
621 self.Scaling = scaling |
621 self.Scaling = scaling |
622 if self.DrawGrid: |
622 if self.DrawGrid: |
623 width = max(2, int(scaling[0] * self.ViewScale[0])) |
623 width = max(2, int(scaling[0] * self.ViewScale[0])) |
624 height = max(2, int(scaling[1] * self.ViewScale[1])) |
624 height = max(2, int(scaling[1] * self.ViewScale[1])) |
625 bitmap = wx.EmptyBitmap(width, height) |
625 bitmap = wx.EmptyBitmap(width, height) |