573 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
573 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
574 self.RefreshView() |
574 self.RefreshView() |
575 |
575 |
576 def RemoveHighlight(self, start, end, highlight_type): |
576 def RemoveHighlight(self, start, end, highlight_type): |
577 highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) |
577 highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) |
578 if (highlight_type is not None and |
578 if highlight_type is not None and \ |
579 (start, end, highlight_type) in self.Highlights): |
579 (start, end, highlight_type) in self.Highlights: |
580 self.Highlights.remove((start, end, highlight_type)) |
580 self.Highlights.remove((start, end, highlight_type)) |
581 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
581 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
582 |
582 |
583 def ShowHighlights(self): |
583 def ShowHighlights(self): |
584 for start, end, highlight_type in self.Highlights: |
584 for start, end, highlight_type in self.Highlights: |