feat: 'Try this' support

[digama0]

Adds proper widget / code action support for "try this" prompts in tactics. Still open: merging the widget into the message itself, depends on leanprover/lean4#2064 .

[fpvandoorn]

Two more things I noticed:

• The tryThisAt in your original code snippet doesn't produce a blue squiggle under the tactic. Is it possible to add this (currently I also use a logInfoAt to produce the squiggle)
• In the implementation of recommend using h I wrote, I put the logInfoAt and tryThisAt both on the word recommend. If I have my pointer at the end of the line, I still see the logInfoAt message that was created on the same line (without opening "All messages"). However, to see the tactic replacements, I need to have my pointer exactly on the word recommend (see screenshot below). Ideally it would show it whenever you are on the same line.
  

[digama0]

@fpvandoorn See whether the new version addresses your concerns. The widget hover (and code action) now happens as long as your cursor is over any of the lines containing the message, same as the messages display.

[Vtec234]

Looks good, all functional issues with the PR that we identified are to be fixed in core rather than here.