vscode-lean4
vscode-lean4 copied to clipboard
Lean Server is missing a way to trigger a move of the cursor to a specified position
We can edit the document via Lsp, but there is no request to the VSCode plugin yet to move the cursor position. revealLocation
and revealPosition
could be made accessible to the server.