diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /ide/coqOps.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r-- | ide/coqOps.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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); |