Skip to content

feat: print the scoped notations correctly - #375

Open
sehun1024 wants to merge 1 commit into
leanprover:mainfrom
sehun1024:main
Open

sehun1024 wants to merge 1 commit into
leanprover:mainfrom
sehun1024:main

Conversation

@sehun1024

@sehun1024 sehun1024 commented Apr 1, 2026

Copy link
Copy Markdown

This PR add a feature to estimate the scope information to print scoped notations correctly.

Now in docgen, there is a known problem that it cannot print the scoped notations.

The main problem was that once the source is compiled, the scope information of the definition are lost, so there is no way to know what scopes to open when printing. This is fine for globally defined notations but it cannot reflect the local notations.

getScopeInfo in this PR finds the source file and do the elaboration which are related to the scope operations (open, namespace...). And if something is defined then it captures the scope and use it when pretty printing.

Note that this is just an estimation, so there may be a possibility to reflect the scope not correctly. To know the exact scope, we should do every elaboration one by one, and that is same as compiling the source again.

I also added some minor build options to skip documentation for core library or to skip this parsing process.

#general > Making docgen print the scoped notations correctly

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.

1 participant