--- 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))