Generate shorter URLs (low priority)

[david-a-wheeler]

The generated URLs for even simple proofs are long. I suspect there will be some system limit we eventually hit.

They shouldn't be so long. I suspect the problem is that they're not getting compressed before being converted. It also suspect the algorithm is really conservative on the symbols it generates for the URL.

It could add EditorCompressedState=... with a more compressed format.

[expln]

It is limited by GitHub. I found it experimentally - only about 5K characters in the editor state (description + vars + disjoints + all steps) may be shared via URLs without problems.

Additional info about encoding currently used in the URL (JFYI):
Such URLs contain a Base64 encoded editor state. It may be decoded with many online Base64 decoders if for some reason a URL is not opened by mm-lamp but it is needed to see its content.

I agree the ability to compress editor state before encoding should be implemented too.

[expln]

I think the ability to download an editor state from some URL similarly how MM databases can be downloaded now may be useful either. In that case you will be able to store the editor state on, for example, Git Hub, and only put its URL inside of mm-lamp URL like editorStateUrl=...

[david-a-wheeler]

The ability to refer to an external URL would be very very awesome. It'd certainly make "click on this link" from within the guide easy to pull off.

That said, it's also awesome to be able to have the whole state embedded in the URL. It's especially useful when you're sharing partial state with someone.