Bug fix: undo now respects the locked area.

Algorithm to fix the bug:
 1. save the status of all the marks
 2. undo
 3. save the status of the cursor after the undo
 4. redo
 5. restore the status of all the marks
 6. if necessary, move the cursor back to its position after the undo
    and perform a goto to unlock the area
 7. perform the undo again

The same algorithm should be applied again to the redo operation!

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 78fbf2f2f25546394dc95b85ff4da5ff8f56c978..38f8cb7849da4d1af0d5cbf2c5328454c6e8f4da 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -198,7 +198,44 @@ class gui () =
       ignore(findRepl#toplevel#event#connect#delete 
         ~callback:(fun _ -> hide_find_Repl ();true));
       ignore(self#main#undoMenuItem#connect#activate
-        ~callback:source_view#source_buffer#undo);
+        ~callback:(fun () ->
+          (* phase 1: we save the actual status of the marks 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#undo ();
+          (* phase 2: we save the cursor position and we redo, restoring
+             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
+           source_view#source_buffer#redo ();
+           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 was 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;
+              source_view#buffer#move_mark `SEL_BOUND ~where:mark_iter;
+              (MatitaScript.instance ())#goto `Cursor ();
+             end;
+            (* phase 4: we perform again the undo. This time we are sure that
+               the text to undo is not locked *)
+            source_view#source_buffer#undo ();
+            source_view#misc#grab_focus ()
+         ));
       ignore(source_view#source_buffer#connect#can_undo
         ~callback:self#main#undoMenuItem#misc#set_sensitive);
       ignore(self#main#redoMenuItem#connect#activate

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 5fa044e5330779cd68f58ce1aa1aa27ccde2f67d..ad4592a67ec028c545afb948c88e5b51a949464a 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -434,6 +434,8 @@ object (self)
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 
+  method locked_mark = locked_mark
+
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)
   method status = match history with hd :: _ -> hd | _ -> assert false

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index 96337cbdb140876585e1e87fc8cd7f0411fe8880..5266a61e04ee1c05ebc0e234cf5360521061f07a 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -26,6 +26,8 @@
 class type script =
 object
 
+  method locked_mark : Gtk.text_mark
+
   (** @return current status *)
   method status: MatitaTypes.status