From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- ide/coqOps.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'ide/coqOps.ml') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index af728471..c7e0810f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -204,7 +204,7 @@ object(self) let on_changed (i, f) = segment#add i (flags_to_color f) in let on_push s = set_index s document_length; - (SentenceId.connect s)#changed on_changed; + ignore ((SentenceId.connect s)#changed on_changed); document_length <- succ document_length; segment#set_length document_length; let flags = List.map mem_flag_of_flag s.flags in @@ -559,7 +559,7 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error "You muse close the proof with Qed or Admitted"; + logger Pp.Error "You must close the proof with Qed or Admitted"; self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> @@ -655,8 +655,6 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; List.iter (fun { start } -> buffer#delete_mark start) seg; @@ -671,7 +669,10 @@ object(self) push_info "Coq is undoing" in let conclusion () = pop_info (); - if move_insert then buffer#place_cursor ~where:self#get_start_of_input; + if move_insert then begin + buffer#place_cursor ~where:self#get_start_of_input; + script#recenter_insert; + end; let start = self#get_start_of_input in let stop = self#get_end_of_input in Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset); -- cgit v1.2.3