diff options
| author | Enrico Tassi | 2017-04-17 10:31:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-24 17:10:25 +0100 |
| commit | e43c35ba795520fe111ac39a834f334753491b28 (patch) | |
| tree | 751a2612627f5b5d4104a5269630e373d66db107 /parsing/pcoq.mli | |
| parent | 9f347ed90495bcde875a5c3646f2291834118a84 (diff) | |
[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>
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 352857d4cd..3203a25b46 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -41,6 +41,16 @@ end - static rules explicitly defined in files g_*.ml4 - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and VERNAC EXTEND (see e.g. file extratactics.ml4) + + Note that parsing a Coq document is in essence stateful: the parser + needs to recognize commands that start proofs and use a different + parsing entry point for them. + + We thus provide two different interfaces: the "raw" parsing + interface, in the style of camlp5, which provides more flexibility, + and a more specialize "parse_vernac" one, which will indeed adjust + the state as needed. + *) (** Dynamic extension of rules @@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list + +(** Parsing state handling *) +val freeze : marshallable:bool -> frozen_t +val unfreeze : frozen_t -> unit |