Pierre Courtieu <pierre.court...@cnam.fr> writes: > Does serapi avoids being based on a notion of document model? Last I > checked about stm it was based on an implicit DAG roughly representing the > lemmas of the file. Don't we need something like that to use serapi > correctly?
It aims to have a simpler notion of document, that must map 1:1 to the editor's buffer. As of today if you send the whole buffer to it, it will partition the buffer in "spans", so you have the notion of span id `sid` that corresponds to a Coq "logical sentence". That's what you use to issue further queries, for example `(Query ((sid 3)) Goals)` This is however not 100% perfect for some reason, so the plan is that SerAPI can also take buffer locations directly, _à la_ LSP, both for document updates and queries. Cheers, E. (*) STM's one is a bit more complicated as it also contains information about scheduling, the thing is that it doesn't map well to a document. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
