Docs moving the operator

Stream: mathlib4

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Pullbacks.html#AlgebraicGeometry.pullbackSpecIso

image.png

Spot the ≅!

[Kenny Lau]

this might be intended?

[Aaron Liu]

It works fine if you have a very wide screen

[Peiran Wu]

Besides the gap, it's really hard to tell which tokens are arguments to pullback and which are on the right hand side of ≅, especially with so many brackets

[Peiran Wu]

I had to read the source to be sure

[Aaron Liu]

Not exactly the most intuitive
image.png

[Christian Merten]

Previous discussion: #general > docgen strange position of equals sign. I recommend to not use the documentation pages when working on algebraic geometry in mathlib, the alignment issue combined with the missing notation for CategoryTheory.CategoryStruct.comp, make the doc pages much harder to read than the source code.

[Kenny Lau]

Christian Merten said:

I recommend to not use the documentation pages when working on algebraic geometry in mathlib

My intention here is to raise issues about the docs so that they could be potentially fixed in the future

[Kyle Miller]

I've looked into trying to fix this before. The issue is that the CSS uses padding and negative text-indent to try to lay things out.

It's an important known issue, but we've been leaving it be for now.

[Weiyi Wang]

if the layout is hard to fix, is it possible to make the doc react to cursor, similar to how infoview does? At least, it can change the background when you move the cursor to show which terms are grouped together. Bonus point if it also displays types as a tooltip

[Kyle Miller]

It looks like there's some CSS there already for adjusting background colors on hover, but it doesn't seem to do anything.