Displaying suggestions with InteractiveCode widget

[0art0]

This PR displays the suggestions from Lean Search as clickable and hoverable expressions in the infoview.

[siddhartha-gadgil]

• From the picture it looks like this is not a "TryThis", so one cannot click or use a code action and replace. Is that correct.
• Also having the types displayed straightaway (as in the current code) is more convenient for a user than having to click.

If I am right about the above they are serious regressions and not worth it for a feature that certainly looks nice but it is not clear how much it helps users in their task of finding results.

[0art0]

Yes, that is correct. Functionality for text replacement on clicking can be added, but it's likely that it will interfere with the hovering functionality.

[siddhartha-gadgil]

Yes, that is correct. Functionality for text replacement on clicking can be added, but it's likely that it will interfere with the hovering functionality.

In that case I am closing this PR. In my view text replacement is something users will want more than hovering before selection.

It would be good to give users choice with multiple commands (or some configuration). But since the additional dependency complicates the use of the present syntax, I suggest you have a different repository with the other format and its use can be discussed separately.