From 5022202a659044d981833ba8665424a52684b07f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 19 Jul 2005 17:22:14 +0000 Subject: [PATCH] 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! --- helm/matita/matitaGui.ml | 39 +++++++++++++++++++++++++++++++++++- helm/matita/matitaScript.ml | 2 ++ helm/matita/matitaScript.mli | 2 ++ 3 files changed, 42 insertions(+), 1 deletion(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 78fbf2f2f..38f8cb784 100644 --- 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 5fa044e53..ad4592a67 100644 --- 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 96337cbdb..5266a61e0 100644 --- 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 -- 2.39.2