Undo/Redo in the popup menu are now working correctly.

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 3e2e8b5fe649d0e314793155ac356d4851e610af..eb75ac11042da2148a198472aebeaa33047583db 100644 (file)
--- 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