- ignore(new_redoMenuItem#connect#activate ~callback:safe_redo);
- ));
- 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);
+ connect_menu_item new_redoMenuItem safe_redo));
+ let clipboard = GData.clipboard Gdk.Atom.clipboard in
+ let text_selected () =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ in
+ let markup_selected () = MatitaMathView.get_selections () <> None in
+ connect_menu_item main#editMenu (fun () ->
+ let text_selected = text_selected () in
+ let markup_selected = markup_selected () in
+ let something_selected = text_selected || markup_selected in
+ main#cutMenuItem#misc#set_sensitive text_selected;
+ main#copyMenuItem#misc#set_sensitive something_selected;
+ main#deleteMenuItem#misc#set_sensitive text_selected;
+ main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None));
+ connect_menu_item main#cutMenuItem (fun () ->
+ source_view#buffer#cut_clipboard clipboard);
+ connect_menu_item main#copyMenuItem (fun () ->
+ if text_selected () then
+ source_view#buffer#copy_clipboard clipboard
+ else if markup_selected () then
+ match MatitaMathView.get_selections () with
+ | None
+ | Some [] -> ()
+ | Some (s :: _) -> clipboard#set_text s);
+ connect_menu_item main#pasteMenuItem (fun () ->
+ source_view#buffer#paste_clipboard clipboard;
+ (MatitaScript.instance ())#clean_dirty_lock);
+ connect_menu_item main#deleteMenuItem (fun () ->
+ ignore (source_view#buffer#delete_selection ()));
+ 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;
+ ignore (findRepl#findEntry#connect#activate find_forward);