Check on scroll (à la Isabelle)

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

GNU Lesser General Public License v2.1

152 stars 32 forks source link

Open Alizter opened 2 years ago

Alizter commented 2 years ago

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.

ejgallego commented 2 years ago

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?

ejgallego commented 2 years ago

ejgallego commented 5 months ago

This is actually implemented by #717 , I'm keeping this issue open for lazy proof checking tho.