Skip to content

feat: use the documentation modifier for docstring semantic tokens - #16314

Open
david-christiansen wants to merge 1 commit into
leanprover:masterfrom
david-christiansen:verso-token-redux
Open

david-christiansen wants to merge 1 commit into
leanprover:masterfrom
david-christiansen:verso-token-redux

Conversation

@david-christiansen

Copy link
Copy Markdown
Contributor

This PR replaces the earlier distinction between text tokens found in docstring and non-docstring Verso content with the consistent use of the documentation modifer for all markup tokens that occur in docstrings. This makes it easier for editors to match a wider variety of themes.

AI assistance was used in this PR to update the tests and review the changes.

This PR replaces the earlier distinction between text tokens found in
docstring and non-docstring Verso content with the consistent use of
the `documentation` modifer for _all_ markup tokens that occur in
docstrings. This makes it easier for editors to match a wider variety
of themes.
@david-christiansen david-christiansen added the changelog-server Language server, widgets, and IDE extensions label Nov 6, 2026
@david-christiansen
david-christiansen removed the request for review from mhuisi November 6, 2026 12:43
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 6, 2026

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant