TextViewer.py
changeset 617 1a80e0598045
parent 616 8a60ffcfd70b
child 619 fc03645162b5
--- 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))