]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
Redo fixed with a strategy similar (but not equal) to the one for undo:
[helm.git] / helm / matita / matitaGui.ml
index 65a18df55c8e8977516e13498bf5c528b217d994..3e2e8b5fe649d0e314793155ac356d4851e610af 100644 (file)
@@ -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 =