Thomas Surrel authored Jul 16, 2020 and Kurt Hindenburg committed Jul 17, 2020

This patch improves the highlightScrolledLines feature in several ways:
- fixes some inconsistences in its behavior
- optimizes the region that needs to be repainted
- fixes cases where the highlight was not cleared correclty when
  changing some  profile properties (e.g. the scroll bar position)