Skip to content

Commit

Permalink
Merge pull request #96 from metamath/explain_temp_mode
Browse files Browse the repository at this point in the history
Explain TEMP mode in tutorial
  • Loading branch information
david-a-wheeler committed Jun 23, 2023
2 parents 1e4ab8e + 83fa702 commit d055752
Showing 1 changed file with 53 additions and 7 deletions.
60 changes: 53 additions & 7 deletions docs/11/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -769,27 +769,73 @@ the proof of the syntax (type) claims as well as the essential steps.
#### Exporting and importing your current state

You can only generate a proof once you *have* a proof.
You can only generate a final proof once you *have* a proof.

Metamath-lamp can export the current state of your efforts,
whatever they are, and anyone can reload them later.
This lets you share details of a proof, even one that isn't complete.
This lets you share your current state, even if that isn't complete.

> Click on the
> icon <img width="16" height="16" src="menu.svg" alt="menu"> (menu)
> on the top right of the display.
This menu includes several ways to export and import your
current state:
You can save your state for reloading later in a JSON format:

* "Export to URL": Provides a URL. You or anyone else
can use this URL to re-open the proof assistant at
this current state.
* "Export to JSON": Provides the current proof assistant
state as text; you can save this where you wish.
* "Import from JSON": Allows you to load a state previously
exported with "Export to JSON".

If you store this information in a file they conventionally
have a `.lamp.json` suffix.

> You can click again on the
> icon <img width="16" height="16" src="menu.svg" alt="menu"> (menu)
> to dismiss the menu.
#### Exporting to URL and temporary mode (TEMP mode)

You can also export the current state into a URL:

> Click on the
> icon <img width="16" height="16" src="menu.svg" alt="menu"> (menu)
> on the top right of the display.
You can then share this URL, to easily share with others your current state.
Anyone who opens this URL can see this state.

**NOTE**: When you open a URL URL exported this way, Metamath-lamp
is opened in *temporary mode (aka TEMP mode)*.
Temporary mode is intended to let you view others' work
*without* erasing your own.
*Changes in temporary mode will not be stored* in
the editor's content to the local storage.
That means closing a browser or any internal error
will erase the editor's content. That's why it is "temporary".

To reduce the risk of accidentally doing something important
while in temporary mode, the web page header starts with "TEMP"
in any tab in temporary mode.
Also, the first attempt to edit will remind you that you're in temporary mode
and that changes will be discarded later. Here is the message
you'll see the first time you try to edit in temporary mode:

> 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.
There's currently no mechanism to switch from temporary (TEMP) mode
to regular mode.
As noted in the warning, if you want to save results from TEMP mode, use
"Export to JSON" to acquire the current state in JSON format.
You can then use "Import from JSON" to load the results into a normal tab.

#### Looking at proof steps

In Metamath, *every* step of a valid completed proof must be an
Expand Down

0 comments on commit d055752

Please sign in to comment.