Emilio Jesús Gallego Arias

This makes the cache much more efficient, with now almost perfect hit rate. However, this also makes obvious the problem we have with our caching system as indeed located messages...

We want to handle this case: ``` Proof. tac1, tacn Qed. ``` Better, so we just don't skip to dot, but can detect the Qed and be smarter here. Note...

Code suggestions

2

In order to try the repair code feature, we can suggest users two hints for `Qed` / `Admitted` proofs: - when the proof is broken, suggest the user to use...

Lazy checking of documents

1

The idea is to allow users to delay proof checking, and do so only under demand, for example when clicking a gutter. There are many heuristics involved here, for example...

See https://code.visualstudio.com/api/language-extensions/language-server-extension-guide#testing-the-language-server for more information, we should add server tests.

Merlin has its own LSP libraries, we should indeed share the code at some point.