Feature Request: wrap on infoview boundaries

leanprover-community / lean4web

The Lean 4 web editor

https://live.lean-lang.org/

Apache License 2.0

52 stars 14 forks source link

Feature Request: wrap on infoview boundaries #10

Closed Seasawher closed 2 months ago

Seasawher commented 7 months ago

Thank you for a nice web editor!

I would like it to be possible to switch whether the code wraps at the right edge or not, as in VSCode.

joneugster commented 2 months ago

Sorry for the long delay. This is now on main, which means it will be on lean.math.hhu.de (our personal test server) tomorrow and on live.lean-lang.org the next time the FRO updates their instance (which happens manually, I think)

Seasawher commented 2 months ago

Thank you!!

nomeata commented 2 months ago

I just deployed this on https://live.lean-lang.org/. Let me know if I broke anything.

nomeata commented 2 months ago

And feel free to ping me on zulip when another update is due