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
13 stars 5 forks source link

Shorten top heading about context #70

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

The top line describing the context is too long on smartphones. It often spills onto 2 lines, which then are permanently spent on the limited vertical space. The user has made database selections by this point, it doesn't need to be so wordy.

So in:

Loaded: set.mm:latest, stopped before '2p2e4'

How about changing "Loaded:" to the symbol 🗄 (🗄 filing cabinet), "stopped before" to "before", and "stopped after" to "through"? I'd remove the comma it seem unneeded. It also doesn't need the quotes around the label, there is nothing else it could be.

That would give more space for useful things.

expln commented 1 year ago

Ok, I see the problem. Actually I knew about it but now it is time to fix it :)

I will hide the heading completely and add a menu item to show it by request. This feature (hiding the heading completely) will be optional and off by default. I don't want to shorten the text. I think it is good for beginners, but for experienced users it is probably not needed at all so it would be better for them to give more space by hiding the heading.

I'd remove the comma it seem unneeded.

Will do.

It also doesn't need the quotes around the label, there is nothing else it could be.

It also could be a raw URL, if no alias specified for it. But I will check this issue with quotes.

expln commented 1 year ago

At the moment I am not ready to shorten the header. Its current version is not short, but this is fine on desktops - the main target of mm-lamp. I implemented ability to hide the context header completely, that should help to work on smartphones.

Moreover, the header text may become even longer in the future. There could be some use cases which are not supported by the header currently but they will have to be supported. For example, when you select "stop before", mm-lamp stops reading before the provided label. But it also closes all the nested blocks. So if there are essential statements in the current block, they disappear from the context after closing all nested blocks. But this may be not correct when loading existing proofs from the context to the editor. I will think on that, but probably the context header will have to indicate somehow if all the nested block were closed or not when mm-lamp stopped reading an MM file.