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

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

1 files changed, 8 insertions, 5 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 716a942d5c..f91aa569d4 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -83,7 +83,10 @@ let set_doc doc = ide_doc := Some doc
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
   let pa = Pcoq.Parsable.make (Stream.of_string s) in
-  let loc_ast = Stm.parse_sentence ~doc sid pa 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
   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
@@ -121,10 +124,10 @@ let query (route, (s,id)) =
 
 let annotate phrase =
   let doc = get_doc () in
-  let {CAst.loc;v=ast} =
-    let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
-    Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
-  in
+  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)