search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
12 stars 5 forks source link

Visualization bug: On visualization, resulting statement is dragged down to next line #116

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

I think there's a minor bug in the visualization display. Let's say I'm using df-2. When visualization is not enabled I see on one line:

✓ 3 P : df-2 |- 2 = ( 1 + 1 )

However, when I enable visualization, there's an unnecessary line break after the justification text : df-2, resulting in:

✓ 3 P : df-2
|- 2 = ( 1 + 1 )
.... (visualization) ...

I think the line break shouldn't happen unless it's necessary.

If this was intentional, can this be a view option? E.g., "Visualizations force linebreak" or something? On small screens display space is a premium, yet I really do want to use the really awesome visualizations.

expln commented 1 year ago

This is just a consequence of the design. That's not a bug, I noticed it from the very beginning and decided to leave it as is. However, I didn't consider this an issue. I designed it in such a way that the statement and visualization are rendered inside of the same div element. Visualizations are often longer than statements. When you open a visualization, the div containing it becomes wider and browser moves it to the next line. So the statement which is also located in this div moves together with it.

I don't have time to change this. So this issue may persist for some longer period of time.