From 8172bc2b4a0116f57f6f986fd5d3478c37a6598b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 08:19:33 +0000
Subject: [PATCH] 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

---
 helm/matita/matitaGui.ml | 39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 65a18df55..3e2e8b5fe 100644
--- 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 =
-- 
2.39.2