--- a/RessourceEditor.py Mon Oct 10 10:14:24 2011 +0200
+++ b/RessourceEditor.py Tue Oct 11 12:07:04 2011 +0200
@@ -71,7 +71,7 @@
def RefreshScaling(self, refresh=True):
pass
- def ClearErrors(self):
+ def ClearHighlights(self):
pass
#-------------------------------------------------------------------------------
@@ -691,26 +691,13 @@
event.Skip()
#-------------------------------------------------------------------------------
-# Search result showing functions
-#-------------------------------------------------------------------------------
-
- def AddShownSearchResult(self, infos, start, end):
- if infos[0] == "task":
- self.TasksTable.AddSearchResult(infos[1:])
- elif infos[0] == "instance":
- self.InstancesTable.AddSearchResult(infos[1:])
-
- def ClearSearchResults(self):
- self.TasksTable.ClearSearchResults()
- self.InstancesTable.ClearSearchResults()
- self.TasksTable.ResetView(self.TasksGrid)
- self.InstancesTable.ResetView(self.InstancesGrid)
-
-
-#-------------------------------------------------------------------------------
# Highlights showing functions
#-------------------------------------------------------------------------------
-
+
+ def OnRefreshHighlightsTimer(self, event):
+ self.RefreshView()
+ event.Skip()
+
def AddHighlight(self, infos, start, end, highlight_type):
if infos[0] == "task":
self.TasksTable.AddHighlight(infos[1:], highlight_type)