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