Merge PR #9263: [STM] explicit handling of parsing states

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes

2 files changed, 14 insertions, 1 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 19ae97da77..759e60fbca 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -439,7 +439,6 @@ module Module =
     let module_expr = Entry.create "module_expr"
     let module_type = Entry.create "module_type"
   end
-
 let epsilon_value f e =
   let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
   let ext = [None, None, [r]] in
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