Improve hover provider

[dlesbre]

Small PR that changes the hover provider a bit:

• Add a newline and a horizontal separator between arg and path section in hover
• Fix hover not appearing at definition sites. Hover now proceeds as follows
  • try getting hover in the context at the start of the current sentence
  • if that fails, try getting hover in the context of the next sentence (newly defined symbols)
  • if that fails, and the next sentence is in proof mode, try using context at next QED (for lemmas and anything defined with tactics).

[rtetley]

Hi @dlesbre, Thanks for your contribution :-) I just rebased your branch on main, is it okay if I force push ? I'll then merge !

[dlesbre]

Sure @rtetley, go ahead !