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

Clarify step type dropdown #132

Closed david-a-wheeler closed 1 year ago

david-a-wheeler commented 1 year ago

Up to this point the step type dropdown has only shown a single letter (P, H, and recently G).

This commit modifies the dropdown to give a slightly longer explanation of what each letter means (if the user doesn't know or remember). It also records the current state, so the current state is highlighted in the dropdown. Hopefully this makes the UI just a little more discoverable and clearer to new users.

david-a-wheeler commented 1 year ago

Done. I think this is better than the original.

It would be nice sometime to be able to see the options immediately on the first long-click instead of having to click the second time. I'm not sure how to do that without changing from a Select though.