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

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

1 files changed, 7 insertions, 6 deletions

diff --git a/stm/stm.mli b/stm/stm.mli
index b6071fa56b..821ab59a43 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -93,16 +93,17 @@ val init_core : unit -> unit
 (** [new_doc opt] Creates a new document with options [opt] *)
 val new_doc  : stm_init_options -> doc * Stateid.t
 
-(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
-   state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t ->
-  Vernacexpr.vernac_control CAst.t
+(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state
+    [sid] and non terminal [entry]. [entry] receives in input the current proof
+    mode. [sid] should be associated with a valid parsing state (which may not
+    be the case if an error was raised at parsing time). *)
+val parse_sentence :
+  doc:doc -> Stateid.t ->
+  entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
 
 (* Reminder: A parsable [pa] is constructed using
    [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
 
-exception End_of_input
-
 (* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
    the state [ontop].
    The [ontop] parameter just asserts that the GUI is on