search

leanprover-community / lean4web

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

Also escape `)` in `code` URL parameter #30

Open nomeata opened 1 week ago

nomeata commented 1 week ago

I just had issues embedding a https://live.lean-lang.org/ url with a code parameter in markdown, presumably because the code contained a closing parenthesis, and thus the URL, and this confused the markdown parser.

For example

https://live.lean-lang.org/#project=lean-nightly&code=%23check%20()

I wonder if this problem would go away if lean4web would also URL-encode the parentheses, e.g.

https://live.lean-lang.org/#project=lean-nightly&code=%23check%20%28%29

These URLs already work, they just have to be generated as such.

joneugster commented 1 week ago

I looked at this once before, for a similar issue.

In particular, the relevant code snippet is to replace encodeURIComponent(content) in this line with a custom function that would also escape %28 and %29.

I think I had a problem that even with this replacement the browser still changed it back, and I'm not sure if this is a browser feature (or Firefox specifically?) , or if I did something wrong. Maybe it's worth trying again!