Show tooltip for the current hovered symbol when the server reply arrives

[gotodev]

Show tooltip for the current hovered symbol when the server reply arrives

[dbolkensteyn]

Implementing this actually seems a bit trickier than what I would have thought initially:

1. Prior to the reply being received, the line of code in the DOM is only split into tokens for the purpose of highlighting: some lines are entirely rendered as a single DOM node
2. Consequently, hovering a single language token will make the entire line DOM node hovered
3. When the server reply arrives, we split the line node into new sub-nodes
4. The issue is that browsers don't seem to recompute the hovered state of those new nodes until the mouse is moved again
5. That makes it difficult to know precisely which new sub-node is currently hovered