- ~callback:self#main#redoMenuItem#misc#set_sensitive);
- let clipboard =
- let atom = Gdk.Atom.clipboard in
- GData.clipboard atom in
- ignore(self#main#cutMenuItem#connect#activate
- ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
- ignore(self#main#copyMenuItem#connect#activate
- ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard));
- ignore(self#main#pasteMenuItem#connect#activate
- ~callback:(fun () ->
- source_view#buffer#paste_clipboard clipboard;
- (MatitaScript.instance ())#clean_dirty_lock));
- ignore(self#main#deleteMenuItem#connect#activate
- ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
- ignore(self#main#findReplMenuItem#connect#activate
- ~callback:show_find_Repl);
- ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ ~callback: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] ->
+ List.iter menu#remove [ copy; cut; delete; paste ];
+ undo,redo
+ | _ -> assert false in
+ let add_menu_item =
+ let i = ref 2 in (* last occupied position *)
+ fun ?label ?stock () ->
+ incr i;
+ GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
+ ()
+ in
+ let copy = add_menu_item ~stock:`COPY () in
+ let cut = add_menu_item ~stock:`CUT () in
+ let delete = add_menu_item ~stock:`DELETE () in
+ let paste = add_menu_item ~stock:`PASTE () in
+ let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
+ copy#misc#set_sensitive self#canCopy;
+ cut#misc#set_sensitive self#canCut;
+ delete#misc#set_sensitive self#canDelete;
+ paste#misc#set_sensitive self#canPaste;
+ paste_pattern#misc#set_sensitive self#canPastePattern;
+ connect_menu_item copy self#copy;
+ connect_menu_item cut self#cut;
+ connect_menu_item delete self#delete;
+ connect_menu_item paste self#paste;
+ connect_menu_item paste_pattern self#pastePattern;
+ 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);
+ connect_menu_item new_undoMenuItem 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);
+ connect_menu_item new_redoMenuItem safe_redo));
+
+ connect_menu_item main#editMenu (fun () ->
+ main#copyMenuItem#misc#set_sensitive self#canCopy;
+ main#cutMenuItem#misc#set_sensitive self#canCut;
+ main#deleteMenuItem#misc#set_sensitive self#canDelete;
+ main#pasteMenuItem#misc#set_sensitive self#canPaste;
+ main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern);
+ connect_menu_item main#copyMenuItem self#copy;
+ connect_menu_item main#cutMenuItem self#cut;
+ connect_menu_item main#deleteMenuItem self#delete;
+ connect_menu_item main#pasteMenuItem self#paste;
+ connect_menu_item main#pastePatternMenuItem self#pastePattern;
+ connect_menu_item main#selectAllMenuItem (fun () ->
+ source_buffer#move_mark `INSERT source_buffer#start_iter;
+ source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
+ connect_menu_item main#findReplMenuItem show_find_Repl;
+ connect_menu_item main#externalEditorMenuItem self#externalEditor;
+ connect_menu_item main#ligatureButton self#nextLigature;
+ ignore (findRepl#findEntry#connect#activate find_forward);
+ (* interface lockers *)
+ let lock_world _ =
+ main#buttonsToolbar#misc#set_sensitive false;
+ develList#buttonsHbox#misc#set_sensitive false;
+ source_view#set_editable false
+ in
+ let unlock_world _ =
+ main#buttonsToolbar#misc#set_sensitive true;
+ develList#buttonsHbox#misc#set_sensitive true;
+ source_view#set_editable true
+ in
+ let locker f =
+ fun () ->
+ lock_world ();
+ try f ();unlock_world () with exc -> unlock_world (); raise exc in
+ let keep_focus f =
+ fun () ->
+ try
+ f (); source_view#misc#grab_focus ()
+ with
+ exc -> source_view#misc#grab_focus (); raise exc in