Add a "reset" option (with "Are you Sure?")

[david-a-wheeler]

Once you're done with a proof, it's not clear how to restart from scratch. You can select and delete all the statements, but that doesn't load a different database. It'd be nice to have a "reset" button, which of course would ask for confirmation (default NO) before erasing everything.

[expln]

I can add a "reset" button but I am not sure that it should reset the database. As for me it will be much handy if this button removes all statements, all variables, disjoins, and description. But leaves currently loaded database untouched.

Changing the database is very simple - click it (I mean click the header) and it will be expanded, then according to what you need either press the "trash can" button, or change the scope and label, add new sources if needed. Then press "Apply changes".

The reason why I think it doesn't make sense to reset the database is how I imaging a usual workflow - load a database, create a proof; delete the proof, create another proof; an so on. With resetting the database users will be forced to load a database again after creating each proof.

[david-a-wheeler]

Okay, that makes sense! Maybe "Are you sure?" dialogue can make that clear. Something like this:

Note: Resetting will erase individual proof information such as the description, variables, disjoins, and
and proof steps. Resetting does not change the current context, that is, the set of loaded databases and their scope. To change the context, go to the context section at the top, modify the context, and press "Apply changes".

[david-a-wheeler]

BTW, I've worked out a simple solution in the editor: use loading. E.g.:

Start up the metamath-lamp application in a completely empty state (erasing whatever you had before in metamath-lamp)

[expln]

Unfortunately this will not work in the next version. Just try to replace latest with dev in this URL and you'll see that mm-lamp opens in TEMP mode. If this approach worked it would be very easy to accidentally erase current editor state just by navigating to another URL (to see some example, or if somebody shared a proof with you and you want to check it in the middle of creating of your own proof).

TEMP mode is read-only. Any change you do in TEMP mode is not saved and will be lost when you close a browser tab with it. This relates to both changes in the editor and in the settings.

Currently there is no easy way how to move from TEMP mode to NORMAL mode. The only way is to 1) use export to JSON in TEMP mode; 2) open a new tab with mm-lamp in NORMAL mode; 3) use import from JSON.

I will add a warning for users when they start editing in TEMP mode, reminding that all their changes will not be saved in this mode.

[expln]

A warning about editing in TEMP mode is implemented on dev. Open mm-lamp on dev by some URL with editorState and try to edit anything in the editor - you will see this warning.

[david-a-wheeler]

Can you tell me more about TEMP mode? What is different about TEMP mode? How do you enter and leave it?

[david-a-wheeler]

Also, what indicates TEMP mode? Just the browser header? The browser header is not normally shown on Firefox on Android, and I don't think it's shown on Macs either.

[david-a-wheeler]

Ah!! Now I see it when I try to edit an existing statement:

Editing in TEMP mode
You are about to edit in TEMP mode. All changes you do in TEMP mode will be erased upon closing current browser tab. If you want to continue editing in NORMAL mode, please do the following actions: 1) use "Export to JSON" to copy current editor state to the clipboard; 2) open a new tab (or switch to an already opened tab) with metamath-lamp in NORMAL mode; 3) use "Import from JSON" to load the copied editor state from the clipboard.

However, I don't see this warning when I press "+" (add statement). Shouldn't this warning also show up the first time you use any modification like add, duplicate, search, replace, renumber?

It looks like "TEMP mode" is forcibly enabled when you load from a URL, correct? That's a little unfortunate for me, because for a tutorial it's nice to be able to reload a specific known state. It'd be nice if there was a way for the URL to say "use this as the real thing" (presumably requiring user confirmation first). I like the idea of a TEMP mode though.

I've drafted guide text to explain this, see the URL below.

[david-a-wheeler]

My attempt to explain TEMP mode is here, please correct as needed:
metamath/lamp-guide#96

[david-a-wheeler]

Related: #114

[expln]

Can you tell me more about TEMP mode? What is different about TEMP mode? How do you enter and leave it?

You've understood it correctly.
The main purpose is not to erase user's work accidentally.
You've also wrote correct instructions in the guide on how to exit TEMP mode (via "export to / import from" JSON).
As of entering, it is also not much convenient but possible: just export to a URL and open this URL :) Yeah, this doesn't work for big states. But if you need to do some experiment without modifying your current state and URL is not enough, you may open a new incognito tab. It has different local storage.

Also, what indicates TEMP mode? Just the browser header? The browser header is not normally shown on Firefox on Android, and I don't think it's shown on Macs either.

For now yes. But I will improve it in scope of #117

However, I don't see this warning when I press "+" (add statement). Shouldn't this warning also show up the first time you use any modification like add, duplicate, search, replace, renumber?

You are right, I missed these cases. I will handle them too. Thanks for pointing this out.

It looks like "TEMP mode" is forcibly enabled when you load from a URL, correct? That's a little unfortunate for me, because for a tutorial it's nice to be able to reload a specific known state. It'd be nice if there was a way for the URL to say "use this as the real thing" (presumably requiring user confirmation first). I like the idea of a TEMP mode though.

Correct, that's how it works now. I implemented TEMP mode even before your first PR in this repo, I didn't expect this need :) Let's discuss this in the corresponding issue you've created #114
(For now, I am going to release v11 with how it works now)

[david-a-wheeler]

(For now, I am going to release v11 with how it works now)

Absolutely! My goal right now is to document it correctly & file issues for my ideas on how I think it could be improved in the future.