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