controls/EditorPanel.py
changeset 617 1a80e0598045
parent 613 c487c54c1cfe
child 635 dbcb8e2d2730
--- a/controls/EditorPanel.py	Sun Jan 08 19:16:58 2012 +0100
+++ b/controls/EditorPanel.py	Sun Jan 08 19:19:42 2012 +0100
@@ -134,6 +134,10 @@
     def RefreshScaling(self, refresh=True):
         pass
 
+    def AddHighlight(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.AddVariableHighlight(infos[1:], highlight_type)
+
     def ClearHighlights(self, highlight_type=None):
         if self.VariableEditor is not None:
             self.VariableEditor.ClearHighlights(highlight_type)