From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 08:19:33 +0000 (+0000)
Subject: Redo fixed with a strategy similar (but not equal) to the one for undo:
X-Git-Tag: V_0_7_2~156
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8172bc2b4a0116f57f6f986fd5d3478c37a6598b;p=helm.git

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 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 =