Clarifing Add and parsing

[gares]

Looking at the code and at Coq pr/204 I think I should clarify.
Today Stm.add is able to add 1 and only 1 sentence, even you pass to it a stream.
Today the grammar of Coq has no entry for a document, so you have to iterate parsing a sentence.

The big problem is that parsing is context dependent. If a sentence is Notation then the following sentence needs the parser to be updated (by executing, at least partially the Notation sentence).
The Stm uses a classification of commands to know which ones alter the parser (labelled as VtNow).

In my, still empty, CEP1 I'd like to propose a document format where phrases altering the parser are
all in the header (Reseve Notation, Import, ...).

JFTR, Isabelle has the (frankly ugly) restriction that terms are written between quotes, as "f x + 3".
These /strings/ can be parsed later on, so the document structure can be fully parsed without altering the parser (the global structure is fixed).

[ejgallego]

Hi Enrico,
thanks for your comment.

The motivation for passing a parsable to Stm.add is not to parse many sentences (we can iterate client side and works fine), but to allow Coq's parser to report accurate location/position.

Note that adding whole documents already works fine, thanks to the STM classification. But the location information is off.

[ejgallego]

Indeed, SerAPI does a bit of a "hack" to report correct location information to the client.

See
https://github.com/ejgallego/coq-serapi/blob/master/sertop/sertop_protocol.ml#L267
we basically parse twice the same document, one with a private stream and other with the STM. #204 would allow us to get rid of that hack.

IMO it would be straightforward to extend Stm.add to parse many sentences, but I'm fine iterating it.

edit: this is incorrect, and the old method was broken

[ejgallego]

I think we can close this. coq/coq#441 implements a reasonable solution for full document parsing, with the important restriction that we can only parse on the tip of the document. This restriction will likely be lifted in the future but for now we can live with it.

Many many thanks to @gares for his very valuable help!