suggestion for the documentation

Stream: mathlib4

[Antoine Chambert-Loir]

I believe it would be nice if mathlib doc pages included, for example on the top of the right column (which is often fixed) the address of the file in mathlib's hierarchy. Of course, that adds yet another piece of information on a page which is already quite full of information.

[Winston Yin (尹維晨)]

The header of each page has the path of the file in the project, e.g. “Mathlib.Data.Core”. Is that what you want?

Until I changed it a few days ago, this same text used to be duplicated as the text of the “return to top” button.

[Winston Yin (尹維晨)]

If I understand correctly, you would like the old behaviour back

[Henrik Böving]

image.png
can you explain more precisely what and where you want it? The name of the module is already in the center top with Init.Prelude and you cn click on the source link at almost the top of the right column so both the module name and source information is present in the site.

[Junyan Xu]

As of a few days ago, the name of the module in the center top doesn't appear unless I shrink the page to 90% (this number may be larger than 100% if you have a wider screen or do not use a vertical tab bar). Below is a comparison between 90% and 100%:
image.png
image.png

[Henrik Böving]

@Winston Yin (尹維晨) I summon you!

[Winston Yin (尹維晨)]

I'll give the classic excuse of "BuT iT wOrKeD oN mY mAcHiNe!"

Jokes aside, I will either make stricter the moment when the header text disappears, or simply restore the hyperlinked document path. I'll make a PR in the next 24 hours. Thanks for bringing this to our attention!

[Winston Yin (尹維晨)]

@Antoine Chambert-Loir Docs updated. The path in the header should remain on even very narrow screens.