941 |
941 |
942 def RemoveHighlight(self, infos, start, end, highlight_type): |
942 def RemoveHighlight(self, infos, start, end, highlight_type): |
943 EditorPanel.RemoveHighlight(self, infos, start, end, highlight_type) |
943 EditorPanel.RemoveHighlight(self, infos, start, end, highlight_type) |
944 |
944 |
945 highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) |
945 highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) |
946 if (infos[0] == "body" and highlight_type is not None and |
946 if infos[0] == "body" and highlight_type is not None and \ |
947 (infos[1], start, end, highlight_type) in self.Highlights): |
947 (infos[1], start, end, highlight_type) in self.Highlights: |
948 self.Highlights.remove((infos[1], start, end, highlight_type)) |
948 self.Highlights.remove((infos[1], start, end, highlight_type)) |
949 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
949 self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True) |
950 |
950 |
951 def ShowHighlights(self, start_pos, end_pos): |
951 def ShowHighlights(self, start_pos, end_pos): |
952 for indent, start, end, highlight_type in self.Highlights: |
952 for indent, start, end, highlight_type in self.Highlights: |