Improve checking resumption on document update (document/didChange)

[ejgallego]

Resumption from the interruption case seems to be working pretty well.

However, for document update, we just restart from the beginning. This can be improved by actually finding a common prefix.

The original idea was to memoize parsing (see #36 and #25 ), however, at least in the current implementation, a much simpler computation of a common prefix would bring the same benefits AFAICS.

[Alizter]

That's a smart idea. In fact we could easily just parse up until a ..

[ejgallego]

In fact we could easily just parse up until a . .

That's interesting, can you provide some more info (or an example) so I'm sure I understand what you mean?

[Alizter]

I mean roughly parse each step in Coq, by comparing prefixes at the . level. I.e.

Goal True.
foo.
bar.

and

Goal True.
foo.
baz.

Would have the same prefix, but only upto

Goal True.
foo.

rather than

Goal True.
foo.
ba

This is a rough approximation, and will suffer when we include statements like { and } but should be more reliable than just checking the text prefix.

[ejgallego]

The whole point of this is to avoid the latency parsing introduces; also note that in general you can't do that because it is perfectly possible that many parts of the document don't parse, also that's tricky due to the way Coq parsing is stateful.

should be more reliable than just checking the test prefix

Interesting, it seems the oposite to me. What is a case where that approach is more reliable that text-prefix?

Note that in a sense, using the common text prefix does get you the previous sentence (with lookup cost linear until we introduce a range map in Doc.t) as indeed you need to resume from a last valid token / state.

But indeed there are many details for this kind of algos so I'm happy to see a PR doing that and understanding how it would compare.