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).
I decided to name the menu item as "Renumber steps" because I don't like how two similar words appear in a row in "Renumber numbered".
Not mentioning "numbered" may make it more difficult for newcomers to understand how renumbering works.
But on the other hand more concise name will be better for experienced users.
Moreover, not understanding why some of the labels are not renumbered is not the only thing which may be not clear for newcomers.
I think it should not be an essential issue.
Also, I decided not to deactivate "Renumber steps" menu item when mm-lamp is not able to renumber.
Instead, if a user lauches the renumbering when it is not possible, a popup appears informing the user why renumbering is not possible.
That will be more helpful than just making the menu item disabled.
This is a logical continuation of another PR https://github.com/expln/metamath-lamp/pull/101
I decided to name the menu item as "Renumber steps" because I don't like how two similar words appear in a row in "Renumber numbered". Not mentioning "numbered" may make it more difficult for newcomers to understand how renumbering works. But on the other hand more concise name will be better for experienced users. Moreover, not understanding why some of the labels are not renumbered is not the only thing which may be not clear for newcomers. I think it should not be an essential issue.
Also, I decided not to deactivate "Renumber steps" menu item when mm-lamp is not able to renumber. Instead, if a user lauches the renumbering when it is not possible, a popup appears informing the user why renumbering is not possible. That will be more helpful than just making the menu item disabled.