diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 39 | ||||
| -rw-r--r-- | ide/session.ml | 28 |
2 files changed, 38 insertions, 29 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index e157696294..608577b297 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -93,23 +93,22 @@ let add ((s,eid),(sid,verbose)) = let pa = Pcoq.Parsable.make (Stream.of_string s) 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_warns ~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, "") + | 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 @@ -136,9 +135,9 @@ let annotate phrase = 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) + | Some ast -> + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v) (** Goal display *) 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 () = |