Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: make all app unexpanders respond to pp.tagAppFns #6730

Merged
merged 2 commits into from
Feb 2, 2025

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Jan 21, 2025

This PR changes how app unexpanders are invoked. Before the ref was .missing, but now the ref is the head constant's delaborated syntax. This way, when pp.tagAppFns is true, then tokens in app unexpanders are annotated with the head constant. The consequence is that in docgen, tokens will be linkified. This new behavior is consistent with how notation defines app unexpanders.

In a followup PR we can slightly simplify the notation unexpander macro to not set the ref.

This PR changes how app unexpanders are invoked, where their ref is initialized to the head constant's delaborated syntax. This way, when `pp.tagAppFns` is true, then tokens in app unexpanders are annotated with the head constant, thus in docgen tokens will be linkified.
@kmill kmill added the changelog-pp Pretty printing label Jan 21, 2025
@kmill
Copy link
Collaborator Author

kmill commented Jan 21, 2025

This PR is more general than #6704. If we go with this solution, we can close that PR.

@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 Jan 21, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 21, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eb30249b1118b5bea767354d5362f4afba97c82e --onto f9e904af5022a57adb6105cda65d1569449346c2. (2025-01-21 18:11:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eb30249b1118b5bea767354d5362f4afba97c82e --onto d68c2ce28bc11ec0271a97aa7a7316905f15a484. (2025-02-02 23:31:30)

@kmill kmill enabled auto-merge February 2, 2025 23:11
@kmill kmill added this pull request to the merge queue Feb 2, 2025
Merged via the queue into leanprover:master with commit 1f6abca Feb 2, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-pp Pretty printing 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.

2 participants