+ 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 ();
+ 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
+ connect_menu_item main#undoMenuItem safe_undo;
+ ignore(source_view#source_buffer#connect#can_undo
+ ~callback:main#undoMenuItem#misc#set_sensitive);
+ connect_menu_item main#redoMenuItem safe_redo;
+ ignore(source_view#source_buffer#connect#can_redo
+ ~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] -> 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);
+ 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));
+ 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);
+ (* 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