# HG changeset patch
# User laurent
# Date 1318327624 -7200
# Node ID 0a6b2e1f8ce3e07a98407d65a79de8b849f2e654
# Parent  1af3cc2b207c64735ad210d5f95ca0cabc642044
Fixing bug in RessourceEditor with highlighting

diff -r 1af3cc2b207c -r 0a6b2e1f8ce3 RessourceEditor.py
--- 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)