ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

[vscode] Add simple commands to move backwards / forward in a proof. #671

Closed ejgallego closed 5 months ago

ejgallego commented 5 months ago

We add two new VSCode commands to allow to move one sentence backwards / forward, this is particularly useful when combined with lazy checking mode

The code is very hacky, and fully client-side, improvements and further ideas most welcome!

Fixes #263, fixes #580.

I'd propose Meta-n and Meta-P as default keybindings, what do you folks think?