[stm] Move main parsing entry point to the STM.

Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.

This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.

This commit supersedes PR#204.

1 files changed, 24 insertions, 17 deletions

diff --git a/stm/stm.mli b/stm/stm.mli
index d3e5dde39..a31e4289d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,24 +13,31 @@ open Loc
 
 (** state-transaction-machine interface *)
 
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop].
-   [check] is called on the AST.
-   The [ontop] parameter is just for asserting the GUI is on sync, but
-   will eventually call edit_at on the fly if needed.
-   The sentence [s] is parsed in the state [ontop].
-   If [newtip] is provided, then the returned state id is guaranteed to be
-   [newtip] *)
-val add :
-  ontop:Stateid.t -> ?newtip:Stateid.t ->
-  ?check:(vernac_expr located -> unit) ->
-  bool -> string ->
-    Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
-
-(* parses and executes a command at a given state, throws away its side effects
-   but for the printings.  Feedback is sent with report_with (defaults to dummy
-   state id)  *)
+(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
+   state [sid] Returns [End_of_input] if the stream ends *)
+val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
+  Vernacexpr.vernac_expr Loc.located
+
+(* Reminder: A parsable [pa] is constructed using
+   [Pcoq.Gram.coq_parsable 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
+   sync, but it will eventually call edit_at on the fly if needed.
+   If [newtip] is provided, then the returned state id is guaranteed
+   to be [newtip] *)
+val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
+  bool -> (Loc.t * Vernacexpr.vernac_expr) ->
+  Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
+   throwing away side effects except messages. Feedback will
+   be sent with [report_with], which defaults to the dummy state id *)
 val query :
-  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
    the requested id is the new document tip hence the document portion following