456     def OnRefreshHighlightsTimer(self, event):

   456     def OnRefreshHighlightsTimer(self, event):

   457         self.RefreshView()

   457         self.RefreshView()

   458         event.Skip()

   458         event.Skip()

   459     

   459     

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

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

   461         if infos[0] == "task":

   463         if infos[0] == "task":

   462             self.TasksTable.AddHighlight(infos[1:], highlight_type)

   464             self.TasksTable.AddHighlight(infos[1:], highlight_type)

   463         elif infos[0] == "instance":

   465         elif infos[0] == "instance":

   464             self.InstancesTable.AddHighlight(infos[1:], highlight_type)

   466             self.InstancesTable.AddHighlight(infos[1:], highlight_type)

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

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