diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/fake_ide.ml | 7 | ||||
| -rw-r--r-- | ide/idetop.ml | 32 |
2 files changed, 28 insertions, 11 deletions
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 8b0c736f50..4e26cb6095 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -241,6 +241,9 @@ let eval_print l coq = | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> let eid, tip = add_sentence ~name phrase in after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"FAILADD"); Tok(_,phrase) ] -> + let eid, tip = add_sentence phrase in + after_fail coq (base_eval_call ~fail:false (add ((phrase,eid),(tip,true))) coq) | [ Tok(_,"GOALS"); ] -> eval_call (goals ()) coq | [ Tok(_,"FAILGOALS"); ] -> @@ -267,7 +270,8 @@ let eval_print l coq = prerr_endline "Quitting fake_ide"; exit 0 | Tok("#[^\n]*",_) :: _ -> () - | _ -> error "syntax error" + | Tok(s,_) :: _ -> error ("syntax error at " ^ s) + | _ -> error ("syntax error") let grammar = let open Parser in @@ -275,6 +279,7 @@ let grammar = let eat_phrase = eat_balanced '{' in Alt [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase] ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] ; Seq [Item (eat_rex "WAIT")] diff --git a/ide/idetop.ml b/ide/idetop.ml index 716a942d5c..205f4455a3 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -64,11 +64,19 @@ let is_known_option cmd = match Vernacprop.under_control cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks ~id {CAst.loc;v=ast} = - let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in - let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in +let ide_cmd_checks ~last_valid {CAst.loc;v=ast} = + let user_error s = + try CErrors.user_err ?loc ~hdr:"IDE" (str s) + with e -> + let (e, info) = CErrors.push e in + let info = Stateid.add info ~valid:last_valid Stateid.dummy in + Exninfo.raise ~info e + in if is_debug ast then - user_error "Debug mode not available in the IDE"; + user_error "Debug mode not available in the IDE" + +let ide_cmd_warns ~id {CAst.loc;v=ast} = + let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_known_option ast then warn "Set this option from the IDE menu instead"; if is_navigation_vernac ast || is_undo ast then @@ -83,11 +91,15 @@ 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 + 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_checks ~id:newid loc_ast; + ide_cmd_warns ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * @@ -121,10 +133,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) |