--- 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)