coq-lsp Check on scroll (à la Isabelle)

Check on scroll (à la Isabelle)

Open Alizter opened this issue 3 years ago • 3 comments

trafficstars

Isabelle is able to check on editor scroll, including not checking the proofs that are not in view.

in #717, we have implemented support for checking document only to the last position scrolled.

Still, skipping Qed. proofs that are not in view remains a TODO.

Jul 06 '22 22:07 Alizter

It would be cool if LSP natively provided us with hints for this, as well as for cursor position. Maybe worth opening an issue upstream?

Jul 06 '22 22:07 ejgallego

See the discussion upstream in https://github.com/microsoft/language-server-protocol/issues/1414#issuecomment-1276590756

Nov 16 '22 01:11 ejgallego