Multiple editor tabs

[CatsAreFluffy]

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]

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.

[expln]

This feature is implemented in the dev version. A new tab TABS has been added. It allows to manage other tabs (create editor and explorer tabs; rename, reorder, and close all tabs). You also can rename active editor and explorer tabs by selecting "rename this tab" menu item in their "hamburger" menus.

[expln]

This feature is available in version 27.