leanprover-community / lean4web

The Lean 4 web editor
https://live.lean-lang.org/
Apache License 2.0
52 stars 14 forks source link

program should be stored in localstore not URL #27

Open rzeta0 opened 1 month ago

rzeta0 commented 1 month ago

As far as I can see the current code is stored in the URL.

I don't believe this will scale to medium-to-longer code.

The web service for prolog https://swish.swi-prolog.org doesn't store code in the URL but appears to store it locally using the web local storage API https://www.w3schools.com/html/html5_webstorage.asp

This has 3 benefits:

Sadly I am no expert at coding so this is a suggestion, not a PR.

joneugster commented 1 month ago

Currently the intended usecase is foremost to be able to easily run small snippets from Zulip and to easily create such MWEs for sharing on the chat service, which is why we are currently always putting the code into the URL.

However, having a share button that creates this URL and using browser storage meanwhile could be an idea.

The drawback might be that you either cannot have multiple tabs with different code open or that you might loose your code on sudden internet loss or accidential reload of the page