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

Automatically start "unify all" after the editor state is loadded #68

Closed expln closed 9 months ago

expln commented 1 year ago

Add optional automatic "unify all" action right after the mm-lamp page loaded. This will add time for the initial loading. So experienced users may turn this off. But for new users this will allow them to see green checkmarks and visualizations without unifying first. This will be useful for small examples distributed via URL.

This also may be implemented via a parameter in the URL. So the author of the URL decides how the page should open. Probably this second option is better.

david-a-wheeler commented 1 year ago

I like this idea!

expln commented 9 months ago

This feature is implemented in version 22. There is a new setting Automatically "Unify All" on the settings tab. It is On by default. When it is On, mm-lamp invokes "unify all" each time the editor content is changed. As a side effect, it closes this issue because this new feature invokes "unify all" after opening an editor by navigating to an mm-lamp URL too.