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

Show fully-qualified name in hover text #811

Merged
merged 3 commits into from
Nov 21, 2021

Conversation

larsk21
Copy link
Contributor

@larsk21 larsk21 commented Nov 19, 2021

Show the fully-qualified name of a declaration when hovering over it. unresolveNameGlobal is changed to return the fully-qualified name when pp.fullNames is set to true, which is the description of this option.

The type shown in the hover is not changed.

semi-closes #749

@Kha
Copy link
Member

Kha commented Nov 19, 2021

Here is a potential issue with the new pp code:

constant foo : Nat

namespace Bar

constant foo : Nat

set_option pp.fullNames true
#check _root_.foo  -- should print `_root_.foo`

end Bar

I think the cleanest solution is to extend your code and duplicate a bit of logic from unresolveNameCore: if pp.fullNames is set, check if resolveGlobalName n₀ resolves to n₀. If it doesn't, prepend rootNamespace.

@Kha Kha merged commit 9028405 into leanprover:master Nov 21, 2021
@larsk21 larsk21 deleted the fully-qualified-hover branch November 22, 2021 08:16
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022
Mathlib3 SHA : 62a5626868683c104774de8d85b9855234ac807c

- [ ] depends on: leanprover#749
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Hover should show full name of declaration
2 participants