[STM] explicit handling of parsing states

DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.

This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.

Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.

Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).

Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

0 files changed, 0 insertions, 0 deletions