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
11 stars 4 forks source link

Multiple editor tabs #153

Open CatsAreFluffy opened 11 months ago

CatsAreFluffy commented 11 months ago

Sometimes when I'm proving a theorem I realize that I need to prove another theorem first. Currently, to do that with metamath-lamp, I need to either export my current state and reimport it later, or open another copy of metamath-lamp in a new tab. It'd be nice if I didn't have to do that.

expln commented 11 months ago

I will think on that. For now, please be aware that when you open another copy of metamath-lamp in a new tab of the same browser it uses the same local storage. This means the second copy overwrites data of the first copy. I would recommend to export the state of the first copy anyway before opening the second one in order not to lose the data from the first copy. If you open the second copy in another browser or in an incognito tab of the same browser then they will be truly distinct and will not overwrite each other.