[parsing] Use AST node for main parsing entry.

Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.

7 files changed, 36 insertions, 39 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index e157696294..608577b297 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -93,23 +93,22 @@ let add ((s,eid),(sid,verbose)) =
   let pa = Pcoq.Parsable.make (Stream.of_string s) in
   match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
   | None -> assert false (* s is not an empty string *)
-  | Some (loc, ast) ->
-  let loc_ast = CAst.make ~loc ast in
-  ide_cmd_checks ~last_valid:sid loc_ast;
-  let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
-  set_doc doc;
-  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  ide_cmd_warns ~id:newid loc_ast;
-  (* TODO: the "" parameter is a leftover of the times the protocol
-   * used to include stderr/stdout output.
-   *
-   * Currently, we force all the output meant for the to go via the
-   * feedback mechanism, and we don't manipulate stderr/stdout, which
-   * are left to the client's discrection. The parameter is still there
-   * as not to break the core protocol for this minor change, but it should
-   * be removed in the next version of the protocol.
-   *)
-  newid, (rc, "")
+  | Some ast ->
+    ide_cmd_checks ~last_valid:sid ast;
+    let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose ast in
+    set_doc doc;
+    let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
+    ide_cmd_warns ~id:newid ast;
+    (* TODO: the "" parameter is a leftover of the times the protocol
+     * used to include stderr/stdout output.
+     *
+     * Currently, we force all the output meant for the to go via the
+     * feedback mechanism, and we don't manipulate stderr/stdout, which
+     * are left to the client's discrection. The parameter is still there
+     * as not to break the core protocol for this minor change, but it should
+     * be removed in the next version of the protocol.
+    *)
+    newid, (rc, "")
 
 let edit_at id =
   let doc = get_doc () in
@@ -136,9 +135,9 @@ let annotate phrase =
   let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
   match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
   | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
-  | Some (_, ast) ->
-  (* XXX: Width should be a parameter of annotate... *)
-  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
+  | Some ast ->
+    (* XXX: Width should be a parameter of annotate... *)
+    Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v)
 
 (** Goal display *)
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 0165b3c029..f6b4593087 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3197,12 +3197,12 @@ let query ~doc ~at ~route s =
       let rec loop () =
         match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
         | None -> ()
-        | Some (loc, ast) ->
-           let indentation, strlen = compute_indentation ~loc at in
+        | Some {CAst.loc; v=ast} ->
+           let indentation, strlen = compute_indentation ?loc at in
            let st = State.get_cached at in
            let aast = {
              verbose = true; indentation; strlen;
-             loc = Some loc; expr = ast } in
+             loc; expr = ast } in
            ignore(stm_vernac_interp ~route at st aast);
            loop ()
       in
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 7f1cca277e..f2025858d7 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -41,7 +41,7 @@ GRAMMAR EXTEND Gram
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None
-              | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) }
+              | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
       ]
     ]
   ;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 45ca658857..ef1dc6993b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,20 +101,18 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
         ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
     with
     | None ->
-        input_cleanup ();
-        state, ids, Pcoq.Parsable.comment_state in_pa
-    | Some (loc, ast) ->
-        let ast = CAst.make ~loc ast in
+      input_cleanup ();
+      state, ids, Pcoq.Parsable.comment_state in_pa
+    | Some ast ->
+      (* Printing of AST for -compile-verbose *)
+      Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
 
-        (* Printing of AST for -compile-verbose *)
-        Option.iter (vernac_echo ~loc) in_echo;
+      checknav_simple ast;
 
-        checknav_simple ast;
+      let state =
+        Flags.silently (interp_vernac ~check ~interactive ~state) ast in
 
-        let state =
-          Flags.silently (interp_vernac ~check ~interactive ~state) ast in
-
-        loop state (state.sid :: ids)
+      loop state (state.sid :: ids)
   in
   try loop state []
   with any ->   (* whatever the exception *)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 0e46df2320..994fad85f0 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
 
     let () =
       let open Extend in
-      let act_vernac v loc = Some (loc, v) in
+      let act_vernac v loc = Some CAst.(make ~loc v) in
       let act_eoi _ loc = None in
       let rule = [
         Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index fa251281dc..4bf7c9f7bd 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
-    val main_entry : (Loc.t * vernac_control) option Entry.t
+    val main_entry : vernac_control CAst.t option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
@@ -40,7 +40,7 @@ module Unsafe : sig
 end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
 
 (** Grammar entry for tactics: proof mode(s).
   By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7611355100..a5ef41c4db 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2167,7 +2167,7 @@ let vernac_load interp fname =
           else
             None
         in
-        interp (snd (parse_sentence proof_mode input));
+        interp (parse_sentence proof_mode input).CAst.v;
       done
     with End_of_input -> ()
   end;