Emilio Jesús Gallego Arias

That's actually not css but JavaScript, we call `scroolIntoView` , indeed, the scroll heuristics could use some tuning, there are often many cases to take into account, for now i...

I think that's possible, nothing in coq-lsp requires you to save the file, right? We could add a command for that, but how would it be different from just creating...

I think that's VSCode choice, not ours. Makes kind of sense tho as it wants to pass to the server a `file:///` uri. So indeed I don't see a way...

We can implement other URI schemes if we would have a need, but we'd need a client for them first.

I am not sure, just trying to figure out, I don't see a way but there could be one. I think they are 3 actions actually that can be done:...

The feature in principle seem sensible to me

The idea I have now is to have a panel where you can see the list of the theories in the workspace, and for each file you can get a...

Dune's memo does something different than what we need (and it is almost of the size of Flèche) Dune's memo does true memoization + scheduling, our `memo.ml` only does the...

Actually it is not easy to control the size of a Hashtbl so that is one of the key difficulties here. Computing the true size can take a long time,...

Hi @tom-p-reichel , I agree that this is not good at all, thanks a lot for documenting your use case. Indexing sentences is actually a bit more tricky than it...