search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
137 stars 25 forks source link

Interface scrolls down, hiding the top #202

Closed noamraph closed 3 months ago

noamraph commented 3 months ago

If I scroll using the mouse wheel, the content continues to scroll up, so I only see the bottom of the interface: image

To reproduce: go to the first level in addition world, zero_add, and type the first line: induction n with d hd.

Something curious: the more I make the window wider, the less blank space there is below the interface. For example, here is what I have with a wider window: image

Perhaps it's related to the inventory box. See this: image Perhaps the white space below is related to the inventory box somehow getting below the interface. When the window is wider, it goes less below the interface, so there is less white space below.

Here's a zip file, the result of "save as HTML (complete)", which shows the problem: nng.zip

joneugster commented 3 months ago

I experienced this once and could never reproduce it.

Can you check if it happens in all levels or only in a few?

The idea about the inventorymight be a good shout... I'll try to investigate

noamraph commented 3 months ago

@joneugster indeed, it seems that it doesn't happen on every stage. It happens to me on the first level of addition world (zero_add), and not on the second (succ_add).

Another clue: it only happens after loading finishes.

I attached a zip file with the "complete HTML", which shows the issue. It might be easier to debug.

And another thing: I just reset the history and got to the first level of addition world, and I don't see this happening. Strange!

noamraph commented 3 months ago

Ok, I now managed to reproduce: you need to enter the first line of the proof, induction n with d hd.

noamraph commented 3 months ago

And another clue: if I add "display: none" to the chat panel (on the left), the white space vanishes.

noamraph commented 3 months ago

Ok, I found it! It's caused by an element <span class="katex-mathml">, which is a part of displaying the stylized "n = 0". Adding display: none to it fixes the issue. The actual "n = 0" is still displayed, thanks to the <span class="katex-html"> element next to it.

noamraph commented 3 months ago

I created a PR which adds the "display: none" CSS to fix the issue: https://github.com/leanprover-community/lean4game/pull/204

joneugster commented 3 months ago

Thanks for the quick PR!