2872     def OnRefreshHighlightsTimer(self, event):

  2872     def OnRefreshHighlightsTimer(self, event):

  2873         self.RefreshView()

  2873         self.RefreshView()

  2874         event.Skip()

  2874         event.Skip()

  2875 

  2875 

  2876     def ClearHighlights(self, highlight_type=None):

  2876     def ClearHighlights(self, highlight_type=None):

  2877         if highlight_type is None:

  2879         if highlight_type is None:

  2878             self.Highlights = []

  2880             self.Highlights = []

  2879         else:

  2881         else:

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

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

  2881         self.RefreshView()

  2883         self.RefreshView()

  2882 

  2884 

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

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

  2884         self.Highlights.append((infos, start, end, highlight_type))

  2888         self.Highlights.append((infos, start, end, highlight_type))

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

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

  2886         

  2890         

  2887     def ShowHighlights(self):

  2891     def ShowHighlights(self):

  2888         for infos, start, end, highlight_type in self.Highlights:

  2892         for infos, start, end, highlight_type in self.Highlights: