vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Lean Server is missing a way to trigger a move of the cursor to a specified position

Open javra opened this issue 2 years ago • 7 comments

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.

javra avatar Jul 19 '22 15:07 javra