791     def OnRefreshHighlightsTimer(self, event):

   791     def OnRefreshHighlightsTimer(self, event):

   792         self.RefreshView()

   792         self.RefreshView()

   793         event.Skip()

   793         event.Skip()

   794 

   794 

   795     def ClearHighlights(self, highlight_type=None):

   795     def ClearHighlights(self, highlight_type=None):

   796         if highlight_type is None:

   798         if highlight_type is None:

   797             self.Highlights = []

   799             self.Highlights = []

   798         else:

   800         else:

   799             highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None)

   801             highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None)

   800             if highlight_type is not None:

   802             if highlight_type is not None:

   801                 self.Highlights = [(infos, start, end, highlight) for (infos, start, end, highlight) in self.Highlights if highlight != highlight_type]

   803                 self.Highlights = [(infos, start, end, highlight) for (infos, start, end, highlight) in self.Highlights if highlight != highlight_type]

   802         self.RefreshView()

   804         self.RefreshView()

   803 

   805 

   804     def AddHighlight(self, infos, start, end, highlight_type):

   806     def AddHighlight(self, infos, start, end, highlight_type):

   805         highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None)

   809         highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None)

   806         if infos[0] == "body" and highlight_type is not None:

   810         if infos[0] == "body" and highlight_type is not None:

   807             self.Highlights.append((infos[1], start, end, highlight_type))

   811             self.Highlights.append((infos[1], start, end, highlight_type))

   808             self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True)

   812             self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True)

   809 

   813