feat: widget messages

[Vtec234]

Allows embedding user widgets in structured messages. Companion PR is leanprover/vscode-lean4#449.

Some technical choices:

• The MessageData.ofWidget constructor might not be strictly necessary as we already have MessageData.ofFormatWithInfos, and there is Info.ofUserWidget. However, .ofUserWidget also requires a Syntax object (as it is normally produced when widgets are saved at a piece of syntax during elaboration) which we do not have in this case. More generally, it continues to be a bit cursed that Elab.Info nodes are used both for elaboration and delaboration (pretty-printing), so entrenching that approach seems wrong. The better approach would be to have a separate notion of pretty-printer annotation; but such a refactor would not be clearly beneficial right now.
• To support non-JS-based environments such as https://github.com/Julian/lean.nvim, .ofWidget requires also providing another message which approximates the widget in a textual form. However, in practice these environments might still want to support a few specific user widgets such as "Try this".

---

Closes #2064.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2bc41d8f3aced0afb6e8d98dbd81d7d7a325da50 --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-23 01:47:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cc33c39cb022d8a3166b1e89677c78835ead1fc7 --onto 66777670e882edde86379fef6914b2938e93b51f. (2024-05-29 06:35:00)