diff -r ccf59c1f0b45 -r c1e5b9f19483 editors/TextViewer.py --- a/editors/TextViewer.py Thu Aug 17 16:26:32 2017 +0300 +++ b/editors/TextViewer.py Thu Aug 17 17:25:17 2017 +0300 @@ -943,8 +943,8 @@ EditorPanel.RemoveHighlight(self, infos, start, end, highlight_type) highlight_type = HIGHLIGHT_TYPES.get(highlight_type, None) - if (infos[0] == "body" and highlight_type is not None and - (infos[1], start, end, highlight_type) in self.Highlights): + if infos[0] == "body" and highlight_type is not None and \ + (infos[1], start, end, highlight_type) in self.Highlights: self.Highlights.remove((infos[1], start, end, highlight_type)) self.RefreshHighlightsTimer.Start(int(REFRESH_HIGHLIGHT_PERIOD * 1000), oneShot=True)