Resolves#4199.
To avoid accidentally highlighting characters that were introduced by
html escaping the text before feeding it to setHtml, we can't just
escape the whole string before adding the highlighting. Instead, we need
to break the string up on the pattern, format and escape the individual
parts, then join them back together.
re.escape includes empty strings if there is a match at the start/end,
which ensures that matches always land on odd indices:
https://docs.python.org/3/library/re.html#re.split
> If there are capturing groups in the separator and it matches at the
> start of the string, the result will start with an empty string. The
> same holds for the end of the string
102c6b99dd