From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- ide/idetop.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'ide') 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) -- cgit v1.2.3