diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 13 |
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) |