diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/fake_ide.ml | 7 | ||||
| -rw-r--r-- | ide/idetop.ml | 63 | ||||
| -rw-r--r-- | ide/session.ml | 28 |
3 files changed, 62 insertions, 36 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..608577b297 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,21 +91,24 @@ 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 - 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; - (* 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, "") + match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with + | None -> assert false (* s is not an empty string *) + | 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 @@ -121,12 +132,12 @@ 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 - (* XXX: Width should be a parameter of annotate... *) - Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) + 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.CAst.v) (** Goal display *) @@ -534,5 +545,5 @@ let islave_init ~opts extra_args = let () = let open Coqtop in - let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in + let custom = { init = islave_init; run = loop; opts = Coqargs.default } in start_coq custom diff --git a/ide/session.ml b/ide/session.ml index 805e1d38a7..e2427a9b51 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -145,10 +145,12 @@ let set_buffer_handlers buffer#apply_tag Tags.Script.edit_zone ~start:(get_start()) ~stop:(get_stop()) end in - let backto_before_error it = + let processed_sentence_just_before_error it = let rec aux old it = - if it#is_start || not(it#has_tag Tags.Script.error_bg) then old - else aux it it#backward_char in + if it#is_start then None + else if it#has_tag Tags.Script.processed then Some old + else if it#has_tag Tags.Script.error_bg then aux it it#backward_char + else None in aux it it in let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); @@ -156,12 +158,16 @@ let set_buffer_handlers let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" + else if it#has_tag Tags.Script.incomplete then + cancel_signal "Altering the script being processed in not implemented" else if it#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if it#has_tag Tags.Script.error_bg then begin - let prev_sentence_end = backto_before_error it in - let text_mark = add_mark prev_sentence_end in - call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) + match processed_sentence_just_before_error it with + | None -> () + | Some prev_sentence_end -> + let text_mark = add_mark prev_sentence_end in + call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); @@ -171,14 +177,18 @@ let set_buffer_handlers let text_mark = add_mark min_iter in let rec aux min_iter = if min_iter#equal max_iter then () + else if min_iter#has_tag Tags.Script.incomplete then + cancel_signal "Altering the script being processed in not implemented" else if min_iter#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" else if min_iter#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if min_iter#has_tag Tags.Script.error_bg then - let prev_sentence_end = backto_before_error min_iter in - let text_mark = add_mark prev_sentence_end in - call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) + match processed_sentence_just_before_error min_iter with + | None -> () + | Some prev_sentence_end -> + let text_mark = add_mark prev_sentence_end in + call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else aux min_iter#forward_char in aux min_iter in let begin_action_cb () = |