Ctrl-click navigation: identifiers remain underlined

[pkapustin]

When the Ctrl key is pressed, identifiers are underlined on mouse hover (as expected).
However, when the Ctrl key is released, the identifiers remain underlined, and the mouse cursor turns to a hand on mouse hover.
The styles usually go back to normal when refresh button is clicked. In the cases when they don't, clicking an identifier makes its style go back to normal.

[Ingo60]

Yes, this happens sometimes, it's a continuos source of displeasure.

Another strange thing is that sometimes the syntax highlighting doesn't work for parts of the source code when there are error marks (that stem from a compilation, that is, after having saved the file)