controls/EditorPanel.py
changeset 738 1ccd08cfae0c
parent 733 c4424d8eebb0
child 761 996515c4b394
--- a/controls/EditorPanel.py	Wed Aug 01 12:44:51 2012 +0200
+++ b/controls/EditorPanel.py	Fri Aug 10 00:32:05 2012 +0200
@@ -130,6 +130,9 @@
             self.Controler.LoadNext()
             self.RefreshView()
     
+    def Find(self, direction, search_params):
+        pass
+        
     def HasNoModel(self):
         return False
     
@@ -157,6 +160,10 @@
         if self.VariableEditor is not None and infos[0] in ["var_local", "var_input", "var_output", "var_inout"]:
             self.VariableEditor.AddVariableHighlight(infos[1:], highlight_type)
 
+    def RemoveHighlight(self, infos, start, end, highlight_type):
+        if self.VariableEditor is not None and infos[0] in ["var_local", "var_input", "var_output", "var_inout"]:
+            self.VariableEditor.RemoveVariableHighlight(infos[1:], highlight_type)
+        
     def ClearHighlights(self, highlight_type=None):
         if self.VariableEditor is not None:
             self.VariableEditor.ClearHighlights(highlight_type)