[BLUEJ-1015] Editor: lines not drawn at correct size after changing font size, visual glitch

See attached screenshots: {quote} Increasing the size will cause some lines to overlay. Clicking on an affected line will fix it. Returning to the default size may keep a gap between two lines.{quote}

!1.png|thumbnail! !2.png|thumbnail! !3.png|thumbnail!

Tested on Windows 10 with HiDPI