diff -r 8a60ffcfd70b -r 1a80e0598045 TextViewer.py --- a/TextViewer.py Sun Jan 08 19:16:58 2012 +0100 +++ b/TextViewer.py Sun Jan 08 19:19:42 2012 +0100 @@ -793,6 +793,8 @@ event.Skip() def ClearHighlights(self, highlight_type=None): + EditorPanel.ClearHighlights(self, highlight_type) + if highlight_type is None: self.Highlights = [] else: @@ -802,6 +804,8 @@ self.RefreshView() def AddHighlight(self, infos, start, end, highlight_type): + EditorPanel.AddHighlight(self, infos, start, end, highlight_type) + highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) if infos[0] == "body" and highlight_type is not None: self.Highlights.append((infos[1], start, end, highlight_type))