Imported Upstream version 8.5~beta3+dfsg

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);