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: Vim Motions #25

Open bernborgess opened 1 month ago

bernborgess commented 1 month ago

How feasible is it to add the vim motions feature? Some web editors support it like replit has these keybinds option: image

It would widely improve the usability of the web editor, and VS Code has plugins for it VSCodeVim VSCode Neovim

joneugster commented 1 month ago

Would that be adding https://github.com/brijeshb42/monaco-vim ?

The underlying editor is a "monaco editor", so one cannot simply "install" vscode extensions.