diff options
-rw-r--r-- | ide/session.ml | 74 |
1 files changed, 40 insertions, 34 deletions
diff --git a/ide/session.ml b/ide/session.ml index e001efc46..e9d4b48ac 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -81,47 +81,52 @@ let create_script coqtop source_buffer = let set_buffer_handlers (buffer : GText.buffer) script (coqops : CoqOps.ops) coqtop = - let call_coq f = - let abort () = - Minilib.log ("Coq busy, discarding query"); - GtkSignal.stop_emit () in - Coq.try_grab coqtop f abort in + let action_was_cancelled = ref true in + let cancel_signal reason = + Minilib.log ("user_action cancelled: "^reason); + action_was_cancelled := true; + GtkSignal.stop_emit () in + let del_mark () = + try buffer#delete_mark (`NAME "target") + with GText.No_such_mark _ -> () in + let add_mark it = del_mark (); buffer#create_mark ~name:"target" it in + let call_coq_or_cancel_action f = + Coq.try_grab coqtop f (fun () -> cancel_signal "Coq busy") in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_insert () = buffer#get_iter_at_mark `INSERT in - let insert_cb it s = - if String.length s > 1 then - let () = Minilib.log "insert_text: Placing cursor" in - let () = buffer#place_cursor ~where:it in - if String.contains s '\n' then - let () = Minilib.log "insert_text: Recentering" in - script#recenter_insert - in - let begin_action_did_not_cancel = ref true in + let insert_cb it s = if String.length s = 0 then () else begin + Minilib.log ("insert_cb " ^ string_of_int it#offset); + let text_mark = add_mark it in + if it#has_tag Tags.Script.to_process then + cancel_signal "Altering to 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)) + end in + let delete_cb ~start ~stop = + Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); + let min_iter = if start#compare stop < 0 then start else stop in + let text_mark = add_mark min_iter in + if min_iter#has_tag Tags.Script.to_process then + cancel_signal "Altering to 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)) in let begin_action_cb () = - begin_action_did_not_cancel := false; - (* We remove any error red zone, and place the [prev_insert] mark *) - let cleanup () = - begin_action_did_not_cancel := true; - let where = get_insert () in + action_was_cancelled := false; + let where = get_insert () in + buffer#move_mark (`NAME "prev_insert") ~where in + let end_action_cb () = + Minilib.log "end_action_cb"; + if not !action_was_cancelled then begin + Minilib.log "cleanup tags"; let start = get_start () in - let () = buffer#move_mark (`NAME "prev_insert") ~where in let stop = buffer#end_iter in buffer#remove_tag Tags.Script.error ~start ~stop; buffer#remove_tag Tags.Script.error_bg ~start ~stop; - buffer#remove_tag Tags.Script.tooltip ~start ~stop in - if (get_insert ())#has_tag Tags.Script.to_process then - GtkSignal.stop_emit () - else if (get_insert ())#compare (get_start()) < 0 then - call_coq (Coq.seq coqops#go_to_insert (Coq.lift cleanup)) - else - cleanup () - in - let end_action_cb () = - let start = get_start () in - let ins = get_insert () in - if !begin_action_did_not_cancel && - 0 <= ins#compare start then Sentence.tag_on_insert buffer - in + buffer#remove_tag Tags.Script.tooltip ~start ~stop; + buffer#remove_tag Tags.Script.processed ~start ~stop; + buffer#remove_tag Tags.Script.to_process ~start ~stop; + Sentence.tag_on_insert buffer; + end in let mark_set_cb it m = let ins = get_insert () in let line = ins#line + 1 in @@ -135,6 +140,7 @@ let set_buffer_handlers in (** Pluging callbacks *) let _ = buffer#connect#insert_text ~callback:insert_cb in + let _ = buffer#connect#delete_range ~callback:delete_cb in let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in let _ = buffer#connect#end_user_action ~callback:end_action_cb in let _ = buffer#connect#after#mark_set ~callback:mark_set_cb in |