Allow people to easily preload an existing proof

[david-a-wheeler]

I think it'd be helpful to allow people to easily preload an existing proof into the prover. Obviously that's not necessary to create a new proof, but there are useful reasons for it:

1. You're new to Metamath & want to see what an existing proof looks like in the tool.
2. You'd like to see the visualizations on an existing proof. The visualizations are really cool, esp. for those new to Metamath.
3. You might want to create a proof that's similar to an existing proof.

If there are already existing statements, there should be a dialogue like "This will erase and replace your existing work. Are you sure you want to do this (y/N)?"

[david-a-wheeler]

E.g., I'd love to tell the tool to load up "2p2e4"; it would then load up to (but not including) 2p2e4, then load the steps to prove 2p2e4.

I find that it's much easier to help people understand how to create proofs by loading up an existing proof, seeing what it looks like, then erasing the steps & seeing if you can re-create it. It's much easier to learn how to do something when there's an answer key of solved problems :-).

[expln]

I am going to implement this. Viewing existing proofs with visualizations will be possible in an embedded proof explorer which I am developing now in develop branch. It will look similar to this - https://expln.github.io/metamath/asrt/2p2e4.html

I already implemented a "temporary mode" - when whatever you edit in the editor does nor override content in another instance of the editor. However, "temporary mode" doesn't store the editor's content to the local storage, so closing a browser (or any internal error) will erase the editor's content. That's why it is "temporary". It is already implemented in develop branch. Initially I implemented it for opening proofs from URLs. But I am going to use it for loading existing proofs too.

[david-a-wheeler]

Visualizations sound interesting!!

However, what I meant here is that you could take an existing proof in a database and load it in as an editable proof. There are reasons to do this:

• This is great for learning - you can load an existing proof, delete some statements, and try to re-prove it
• It's also great for trying to improve a proof, e.g., to make it shorter or remove use of an axiom.
• It also would make it easier to split a proof into smaller pieces (e.g., to pull out a lemma).

[david-a-wheeler]

Please do NOT use temporary mode when loading a proof ("Import from JSON"). Otherwise there's no easy way to store state for it to be easily reloaded later. "Import from JSON" is basically the only way to reload current state into a different browser. I routinely switch between my laptop and my phone, for example.

[expln]

I will not use TEMP mode when loading a proof. TEMP mode is used only when it is very easy to load a proof, for example, by clicking a link. Loading from JSON and loading an existing proof from the current context (this feature is to be implemented yet) is not so easy and users are expected to understand what they are doing, so no need in TEMP mode in these cases.