Redo fixed with a strategy similar (but not equal) to the one for undo:

1. we save the position of all the marks
2. we redo
3. we undo
4. we save the position of the cursor after the undo
5. if necessary, we restore the initial position of all the marks,
   we move the cursor to its position after the undo and then we goto
6. we redo

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 65a18df55c8e8977516e13498bf5c528b217d994..3e2e8b5fe649d0e314793155ac356d4851e610af 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -238,7 +238,44 @@ class gui () =
       ignore(source_view#source_buffer#connect#can_undo
         ~callback:self#main#undoMenuItem#misc#set_sensitive);
       ignore(self#main#redoMenuItem#connect#activate
-        ~callback:source_view#source_buffer#redo);
+        ~callback:(fun () ->
+          (* phase 1: we save the actual status of the marks, we redo and
+             we undo *)
+          let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+          let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+          let locked_iter_offset = locked_iter#offset in
+          let mark2 =
+           `MARK
+             (source_view#buffer#create_mark ~name:"lock_point"
+               ~left_gravity:true locked_iter) in
+          source_view#source_buffer#redo ();
+          source_view#source_buffer#undo ();
+          (* phase 2: we save the cursor position and we restore
+             the previous status of all the marks *)
+          let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+          let mark =
+           `MARK
+             (source_view#buffer#create_mark ~name:"undo_point"
+               ~left_gravity:true cursor_iter)
+          in
+           let mark_iter = source_view#buffer#get_iter_at_mark mark in
+           let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+           let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+            source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+            source_view#buffer#delete_mark mark;
+            source_view#buffer#delete_mark mark2;
+            (* phase 3: if after the undo the cursor is in the locked area,
+               then we move it there again and we perform a goto *)
+            if mark_iter#offset < locked_iter_offset then
+             begin
+              source_view#buffer#move_mark `INSERT ~where:mark_iter;
+              (MatitaScript.instance ())#goto `Cursor ();
+             end;
+            (* phase 4: we perform again the redo. This time we are sure that
+               the text to redo is not locked *)
+            source_view#source_buffer#redo ();
+            source_view#misc#grab_focus ()
+         ));
       ignore(source_view#source_buffer#connect#can_redo
         ~callback:self#main#redoMenuItem#misc#set_sensitive);
       let clipboard =