equal
deleted
inserted
replaced
132 self.ParentWindow._Refresh(*args) |
132 self.ParentWindow._Refresh(*args) |
133 |
133 |
134 def RefreshScaling(self, refresh=True): |
134 def RefreshScaling(self, refresh=True): |
135 pass |
135 pass |
136 |
136 |
|
137 def AddHighlight(self, infos, start, end, highlight_type): |
|
138 if self.VariableEditor is not None and infos[0] in ["var_local", "var_input", "var_output", "var_inout"]: |
|
139 self.VariableEditor.AddVariableHighlight(infos[1:], highlight_type) |
|
140 |
137 def ClearHighlights(self, highlight_type=None): |
141 def ClearHighlights(self, highlight_type=None): |
138 if self.VariableEditor is not None: |
142 if self.VariableEditor is not None: |
139 self.VariableEditor.ClearHighlights(highlight_type) |
143 self.VariableEditor.ClearHighlights(highlight_type) |