feat: extensible Markdown rendering of Verso docstrings

[david-christiansen]

This PR adds support for extensible Markdown rendering of Verso docstrings.

Markdown rendering is used when docstrings are prepared for LSP hovers as well as for legacy clients that don't directly support Verso. Previously, when the docstring contained a custom element, Markdown rendering simply delegated to the alternate fallback rendering. Now, the custom elements can have custom rendering to Markdown.

Example use cases include:

• Including a docstring in another: with the module system, docstrings are part of the server olean and are loaded only in interactive sessions. If one docstring is to include another, it must be fetched at a time when the docstrings are loaded and available. A custom element can save which docstring is to be included at elaboration time, and then look it up at rendering time.

• Showing a list of all currently-available instances of a class.

• Showing names with respect to the currently-open namespaces.

• Custom links to e.g. library notes that look up the destination in an environment extension.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 22:36:36)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-18 22:36:38)