From b6e1e47a8fdb45e9e47af9dfd047a0241ecf59c1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Jul 2005 12:46:25 +0000 Subject: [PATCH] Undo/Redo in the popup menu are now working correctly. --- helm/matita/matitaGui.ml | 183 +++++++++++++++++++++++---------------- 1 file changed, 107 insertions(+), 76 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 3e2e8b5fe..eb75ac110 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -197,87 +197,118 @@ class gui () = connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ()); ignore(findRepl#toplevel#event#connect#delete ~callback:(fun _ -> hide_find_Repl ();true)); - ignore(self#main#undoMenuItem#connect#activate - ~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 + let safe_undo = + 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; + (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 (); - (* 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; - (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 () - )); + source_view#misc#grab_focus () in + let safe_redo = + 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 () + in + ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo); ignore(source_view#source_buffer#connect#can_undo ~callback:self#main#undoMenuItem#misc#set_sensitive); - ignore(self#main#redoMenuItem#connect#activate - ~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(self#main#redoMenuItem#connect#activate ~callback:safe_redo); ignore(source_view#source_buffer#connect#can_redo ~callback:self#main#redoMenuItem#misc#set_sensitive); + ignore(source_view#connect#after#populate_popup + ~callback:(fun pre_menu -> + let menu = new GMenu.menu pre_menu in + let menuItems = menu#children in + let undoMenuItem, redoMenuItem = + match menuItems with + [undo;redo;sep1;cut;copy;paste;delete;sep2; + selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo + | _ -> assert false in + let new_undoMenuItem = + GMenu.image_menu_item + ~image:(GMisc.image ~stock:`UNDO ()) + ~use_mnemonic:true + ~label:"_Undo" + ~packing:(menu#insert ~pos:0) () in + new_undoMenuItem#misc#set_sensitive + (undoMenuItem#misc#get_flag `SENSITIVE); + menu#remove (undoMenuItem :> GMenu.menu_item); + ignore(new_undoMenuItem#connect#activate ~callback:safe_undo); + let new_redoMenuItem = + GMenu.image_menu_item + ~image:(GMisc.image ~stock:`REDO ()) + ~use_mnemonic:true + ~label:"_Redo" + ~packing:(menu#insert ~pos:1) () in + new_redoMenuItem#misc#set_sensitive + (redoMenuItem#misc#get_flag `SENSITIVE); + menu#remove (redoMenuItem :> GMenu.menu_item); + ignore(new_redoMenuItem#connect#activate ~callback:safe_redo); + )); let clipboard = let atom = Gdk.Atom.clipboard in GData.clipboard atom in -- 2.39.2