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

[dbolkensteyn]

This issue mostly arises on PRs where the server reply takes a few seconds to arrive:

• If a symbol is hovered before the reply arrives, nothing is shown, as expected
• However, when the reply finally arrives, it should make sense to show the tooltip

Reproducer:

• Try to quickly hover the ObjectMapper symbol on this link: https://github.com/dadoonet/legacy-search/blob/01-direct/src/main/java/fr/pilato/demo/legacysearch/dao/ElasticsearchDao.java#L22
• Keep it hovered, nothing ever happens
• Move the mouse away and back on ObjectMapper, and the tooltip is then shown.

[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